Prove exact star budgets for prescribed odd-unicyclic targets (no κ)

research/odd-unicyclic-star-budgets/PROOF.md

@@ -0,0 +1,161 @@
+# Exact budgets for prescribed targets with one odd cycle
+
+This scoped theorem was produced by Nick Petalas. It extends Sam Sung's
+[graph-target note](../asymmetric-hypercube-decoder/GRAPH-TARGETS.md), from
+PR #669. That note supplies the observation model, the unit-row criterion,
+the general nonzero-constant lower bound, and the triangle specialization.
+The new contribution is attainment for every prescribed target set with
+exactly one cycle in total, provided that cycle is odd. The lower-bound
+argument is included to make the extension readable on its own.
+
+## Statement
+
+Let p >= 3, and let G be the complete graph on n = 2p vertices with a
+perfect matching removed. Its E = 2p(p-1) edges are the signed two-ports.
+All vector spaces in this note are over F2.
+
+For a retained edge set F, the available observations are the vertex sums
+
+    star_v(F) = sum_{e in F, v in e} x_e
+
+and the empty star `sum_{e in F} x_e`. This is the source's C+ code. At k=2,
+the permitted overlap correction for target uv is star_u + star_v and
+therefore adds no observation. Every retained input x_e is arbitrary and
+independent.
+
+Let T be a prescribed target edge set. Assume the spanning graph with edges
+T has exactly one cycle in total, of odd length. It may also have trees
+attached to that cycle, other tree components and isolated vertices.
+Write r = |T| and s = n-r+1, the number of components of T, including
+isolated vertices. Then the minimum number of deleted edges disjoint from
+T that makes every x_t, t in T, individually recoverable is
+
+    delta_+(T) = 2p(p-1) - r - floor((2p-r+1)^2 / 4).          (1)
+
+In particular, the optimum depends only on p and r within this class.
+Formula (1) applies to every p, with no upper bound imposed by the finite
+checker. Without the empty star such a cyclic target set is infeasible,
+as already proved in the source's feasibility criterion.
+
+## The inherited lower bound
+
+Combine r individual unit decoders into a vector decoder. It assigns each
+vertex v a coefficient a_v in F2^r and the empty star a coefficient b.
+At a retained edge uv the coefficient is a_u + a_v + b. It must be the
+corresponding standard basis vector e_t for t in T and zero on every
+retained nontarget edge. If recovery uses arbitrary exact postprocessing of
+these linear observations, the same criterion still applies: an input
+coordinate recoverable on every input vanishes on the observation kernel,
+and hence belongs to its row space.
+
+Summing the target equations around the unique odd cycle gives
+
+    b = sum_{t on the cycle} e_t != 0.                       (2)
+
+Let H be the retained nontarget graph, with h components including isolated
+vertices. On every edge of H, a_u + a_v = b. Thus H is bipartite. In each
+component choose a root with coefficient c_i and write
+a_v = c_i + sigma_v b, where sigma_v is the path parity from that root.
+The target coefficients all lie in the span of b and the vectors c_i+c_j.
+This span has dimension at most h, because the latter vectors are spanned
+by c_i+c_1 for 2 <= i <= h. The r target coefficients are independent, so
+h >= r.
+
+A bipartite component with v vertices has at most f(v)=floor(v^2/4) edges.
+Put g(t)=f(t+1) for integers t >= 0. Then g(0)=0, and the successive
+increments of g are 1,1,2,2,3,3,... . They are nondecreasing, so
+g(a)+g(b) <= g(a+b) for a,b >= 0. Consequently, for component sizes v_i,
+
+    |H| <= sum_i g(v_i-1)
+         <= g(n-h)
+         <= g(n-r) = floor(s^2/4).                          (3)
+
+At most r+floor(s^2/4) edges can remain. Subtracting from E proves the
+lower bound in (1). This is the source's nonzero-constant bound applied
+to a target set that forces b != 0, rather than a new lower-bound method.
+
+## Choosing a balanced root set despite the missing matching
+
+Choose one root from each component of T. We need a choice R of s roots
+and a partition R=A disjoint-union B with
+
+    |A|=floor(s/2), |B|=ceil(s/2),
+
+such that no removed matching edge has one endpoint in each part.
+
+For any root set, group its complete matched pairs into atoms of size two,
+and its unmatched root vertices into atoms of size one. Keeping each atom
+in one part prevents every forbidden crossing.
+
+If there is at least one singleton atom, every integer size from zero to s
+is a sum of atom sizes. Indeed, if there are a double atoms and b >= 1
+singletons, the intervals [2j,2j+b], for 0 <= j <= a, cover all integers
+from zero to 2a+b. Thus the balanced partition exists. If every atom has
+size two and s is divisible by four, it also exists.
+
+The only remaining case is a root set made entirely of complete matched
+pairs, with s congruent to 2 modulo 4. There is a nontrivial target
+component, since T contains an odd cycle. Replace its chosen root v by
+another vertex w in that component. Initially R is a union of complete
+matched pairs. Since w was not a root, neither was its mate. Since v was
+a root, its mate was a root in another component. After the replacement,
+w and the mate of v are singleton atoms. The preceding argument applies.
+The replacement preserves one root per target component.
+
+This proves the required root-selection statement for all s >= 1. When
+s=1, A is empty and B consists of the sole root.
+
+## Attaining the bound with literal decoder coefficients
+
+Take R,A,B as above, and let H contain every edge between A and B. All
+these edges exist in G. They are nontarget edges because distinct roots
+belong to distinct target components. Therefore
+
+    |H|=|A||B|=floor(s^2/4),   F=T disjoint-union H.
+
+Here is a direct construction of the unit decoders, including their empty
+star coefficients. Define b by (2). Set a_v=b at every root in A and
+a_v=0 at every root in B. Remove one edge t_0 of the target cycle, leaving
+a spanning tree in each target component. Traverse those trees outward
+from the selected roots. For a tree edge t=uv, with u already assigned, set
+
+    a_v = a_u + b + e_t.                                   (4)
+
+All retained tree edges now have their desired coefficient. Along the
+path replacing t_0 there are an even number of edges, because the removed
+cycle is odd. Summing (4) along that path gives
+
+    a_u + a_v + b = sum_{t on cycle, t != t_0} e_t + b
+                  = e_(t_0).
+
+So the omitted cycle edge also has its unit coefficient. At any edge of
+H, one root has label b and the other zero, giving coefficient b+0+b=0.
+Each coordinate of this vector identity is an actual decoder for one
+prescribed target using the allowed observations on F. Every retained
+nontarget input has coefficient zero, without an input restriction.
+
+Exactly r+floor(s^2/4) edges remain. Together with (3), this proves (1).
+
+## A first case beyond the source's triangle formula
+
+At p=3 let T be the five-cycle 0,2,1,4,3,0, with vertex 5 isolated. All
+five target edges are allowed. Here r=5, s=2 and E=12. Take roots 0 and 5,
+so H consists of the single edge 05. The construction retains six edges
+and deletes six. Bound (3) proves that fewer than six deletions cannot
+suffice. No triangle is present in this target graph.
+
+For a triangle with all other vertices isolated, r=3 gives
+delta_+=p^2-4, recovering the source's already proved result with credit.
+The added scope includes longer odd cycles and arbitrary tree additions.
+
+## Scope
+
+This is a uniform algebraic proof with finite corroboration. The code
+constructs coefficients; it does not implement the observations as paid
+native operations. Physical frames, helper acquisition, dirty restoration,
+tape movement, precision, recursive prices and the complete multiplication
+theorem remain separate obligations. No new kappa is claimed.
+
+New proof and checker are Apache-2.0. The source credits the graph-incidence
+bridge to Martinez-Bernal, Valencia-Bucio and Villarreal, and retains Joel
+Pulikkan / GamingPuzzled, icekylinx and eumemic's paired-cube lineage.

research/odd-unicyclic-star-budgets/README.md

@@ -0,0 +1,112 @@
+# Exact star budgets for prescribed targets with one odd cycle
+
+Scoped uniform proof with finite exact corroboration. In the binary signed
+two-port observation model of [Sam Sung's PR #669](https://github.com/CrocSwap/integer-mult-bounds/pull/669),
+allow every vertex star and the empty star. If the prescribed target graph
+has exactly one cycle in total, and that cycle is odd, its exact deletion
+budget is
+
+```text
+delta_+(T) = 2p(p-1) - r - floor((2p-r+1)^2/4),  r = |T|.
+```
+
+Attached trees, other tree components and isolated vertices are allowed.
+The theorem holds for every p >= 3. A five-cycle on six vertices needs
+exactly six deletions; the source's triangle formula is the r=3 special
+case. Within this class, the optimum depends only on p and r.
+
+The source already supplies the general nonzero-constant lower bound and
+the triangle optimum. The new step is a balanced root construction that
+attains that bound for the whole odd-unicyclic class, despite the removed
+perfect matching. [PROOF.md](PROOF.md) supplies the uniform argument and
+literal vector-valued decoder coefficients. Predecessor results are cited,
+not audited or replayed as the contribution.
+
+This is a scalar observation result. It supplies no paid supplier, physical
+frame schedule, helper preparation, dirty restoration, precision/tape bill
+or new kappa. The selected result and its five framework assumptions remain
+unchanged. Independent human and formal proof-kernel review are unclaimed.
+
+## Evidence
+
+The independent small-instance oracle enumerates all 4,096 retained graphs
+at p=3, computes their observation row spaces, and optimizes every target
+set by a superset transform. All 864 eligible target sets agree with the
+formula and the constructed coefficients. By target count r=3,4,5,6 there
+are respectively 8,72,288,496 sets. The matching obstruction triggers the
+root replacement on 128 of these sets.
+
+The constructor also checks 2,704 fixed fixtures at p=4,...,16, covering
+every odd cycle length from 3 through 31, attachments and separate tree
+components. These are fixture cases, with repetition allowed, rather than
+a census of all larger target graphs. Every one of their 101,231 retained
+input columns has its literal required coefficient.
+
+Controls reject five invalid target inputs, three decoder mutations and
+all twelve single-edge restorations of the displayed p=4 triangle witness.
+The component-concentration inequality is also checked on 1,600 integer
+pairs. These finite checks corroborate the written proof; they do not
+replace its all-size quantifiers. The verifier imports no predecessor code.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/odd-unicyclic-star-budgets/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/odd-unicyclic-star-budgets/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/odd-unicyclic-star-budgets
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/odd-unicyclic-star-budgets --check-source-history
+```
+
+Another CPython 3.12 executable can replace that local interpreter path.
+The marker is `PASS_ODD_UNICYCLIC_STAR_BUDGETS`, followed by enumerated
+coverage and SHA256 hashes. `--receipt /absolute/new/file.json` writes a
+new source-bound receipt outside the package and refuses overwrite.
+The default verifier writes nothing. Registered normal and optimized
+commands each have a 120-second limit.
+
+[SOURCES.json](SOURCES.json) pins the exact main-branch predecessor note;
+the shared metadata runner authenticates its working bytes and historical
+provenance. The direct mathematical checker needs only this package and
+does not consume the predecessor's implementation. The original catalogue
+card and selected record are retained as historical provenance. The changed
+scope from a native-register construction to an algebraic side result is
+explicit in [TASK.json](TASK.json).
+
+## Open next questions
+
+What is the exact C+ budget for a prescribed forest with r>p? The source
+gives a C- matching formula and a uniform no-benefit result for C+ when
+p>=6 and r<=p. Start with one p>=6 forest above that range and compare
+the matching optimum with the nonzero-constant bipartite bound. A forest
+does not force a nonzero empty-star coefficient, so both decoder types
+must be considered. This question is left unclaimed.
+
+## Engineering limits
+
+All scientific loops have explicit finite domains. Constructor fixtures
+validate 2<=p<=20, giving at most forty vertices and 760 edges. The largest
+exhaustive arrays have 4,096 entries. The proof has no such p limit.
+Functions are below sixty lines; all checks use exceptions and remain
+active under optimization. No recursion or subprocess is used.
+
+Power-of-Ten rule 3 has a managed-runtime deviation: CPython and its standard
+library allocate during replay. Live collections are bounded by the above
+input limits, receipts contain bounded aggregates, and the shared runner
+enforces the timeout. Extending the finite domain requires reassessing
+those capacities. Rule 9 has a bounded test-only dispatch deviation:
+rejection controls call the local analyze and endpoint functions through
+fixed lambdas. The target set of those callbacks is explicit and contains
+no external code. Warning-strict normal and optimized execution provide
+the available interpreter diagnostics; no external linter is required.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Sam Sung /
+the-missionary-company retains credit for PR #669's observation model,
+graph-target reductions, inherited lower bound and triangle result.
+The graph-incidence bridge retains Martinez-Bernal, Valencia-Bucio and
+Villarreal's credit. Joel Pulikkan / GamingPuzzled, icekylinx and eumemic
+retain the paired-cube lineage. The new attainment proof, constructor and
+independent finite oracle are the contribution here. New work is Apache-2.0.

research/odd-unicyclic-star-budgets/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/asymmetric-hypercube-decoder/GRAPH-TARGETS.md",
+      "usage": "input",
+      "git_blob": "65b566326ebb213ff013b3825ce9f432dfff5bae",
+      "sha256": "a9f14398ccf6490af546becb4ef744217594650bbb68450665ff47ccc14397f5"
+    }
+  ]
+}

research/odd-unicyclic-star-budgets/TASK.json

@@ -0,0 +1,76 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact prescribed-target deletion budgets in the binary signed two-port C+ observation code, for every target graph with exactly one odd cycle in total.",
+  "scope_change_reason": "The native larger-register card is changed to a self-contained algebraic decoder side result. PR669 gives exact forest and triangle budgets but not the attaining construction for general odd-unicyclic targets.",
+  "bottleneck_link": "A sharp scalar observation threshold constrains which prescribed jobs can share these observations before a physical supplier is priced. This does not change the actual selected E8 or BIT supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first uniform exact budget is proved and independently corroborated on every six-vertex retained graph; package it without extending to other target classes.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, exact exhaustive p=3 oracle, literal larger-fixture decoder columns and rejection controls in verify.py.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the exact C+ deletion budget for a prescribed target forest with r>p?",
+      "why_it_matters": "PR669 supplies a general partition optimization and a C- matching formula, while its uniform no-benefit result for C+ covers r<=p at p>=6.",
+      "first_step": "Compare the nonzero-constant bipartite bound against the C- matching optimum for one p>=6 forest with r>p.",
+      "blocked_by": "A forest does not force the empty-star coefficient to be nonzero, so both decoder types must be optimized."
+    }
+  ],
+  "predecessor_credit": {
+    "source": "PR #669, Sam Sung / the-missionary-company",
+    "new_step": "Uniform attainment of the inherited nonzero-constant bound for every odd-unicyclic prescribed target set."
+  },
+  "orientation": "research_selected_baseline.py passed source bindings for selected PR6030, kappa 781451/250000000; no scientific replay.",
+  "environment": {
+    "python": "3.12.15",
+    "implementation": "CPython",
+    "system": "Darwin",
+    "machine": "arm64",
+    "dependencies": "standard library only"
+  }
+}