Prove exact six-call nonunit fanout on a directed cycle (no κ)

research/z4-directed-cycle-fanout/PROOF.md

@@ -0,0 +1,73 @@
+# Six is the exact directed-cycle price
+
+Let R=Z/4, w>=1 and take arbitrary independent a,b,c,p in R^w. The dirty
+rows start at a,b,c. The disjoint source p cannot be written. The gate
+E_ij(alpha) adds alpha A_j into A_i, for distinct dirty rows i,j; P_i(beta)
+adds beta p into A_i. Every nonzero coefficient is allowed. The gate types
+E_10, E_21, E_02 and P_0 cost one; the remaining five types cost 100.
+Prices are stationary and coefficient-independent. No other operations,
+workspace, observations or free basis changes are available. Words are fixed,
+finite and may have arbitrary repetitions and interleavings. The required
+endpoint is (a+2p,b+p,c+p,p) on every input.
+
+## Attainment
+
+Execute chronologically
+
+```text
+E_21(-1), E_10(-1), P_0(1), E_10(1), P_0(1), E_21(1).
+```
+
+The first two gates leave (a,b-a,c-b). After the first insertion and next
+ADD they are (a+p,b+p,c-b). The last insertion and ADD give
+(a+2p,b+p,c+p). Every gate costs one; the complete price is six. The source
+never changes. The identities hold coordinatewise at every positive width,
+retaining all original dirt.
+
+## No word can cost less
+
+Track the three-by-three matrix M of original dirt coefficients. Every
+prefix is invertible, because each ADD has its negated-coefficient inverse
+and insertions leave M unchanged. The endpoint requires M=I.
+
+Recall the incoming-row return argument of #5045/#5163. A row cannot receive
+exactly one nonzero ADD. Before its unique incoming ADD its dirt row is e_i.
+If that gate is E_ij(alpha), restoration with no later incoming ADD requires
+alpha m_j=0, where m_j is row j of the invertible prefix M. Right multiplication
+by M inverse gives alpha e_j=0, hence alpha=0, a contradiction. This counts
+total arrivals at a row, not individual directed edges.
+
+Suppose a word costs less than six. It uses only price-one gates, so every
+source insertion is into row zero. Let t be the number of insertions. Rows
+one and two each have a nonzero final source coefficient and no insertion
+of their own. Each must receive an ADD, hence at least two by the return
+argument.
+
+If t=0, every source coefficient remains zero, which is impossible. If
+t>=2, its price is at least t+2+2>=6, a contradiction.
+
+For t=1, write beta for the inserted coefficient. The final source column
+is beta v, since every subsequent gate is R-linear. Its row-one coefficient
+is 1, so beta is a unit. If row zero receives no ADD, its final source
+coefficient is beta, which cannot equal the required nonunit 2. Row zero
+therefore receives at least one ADD, and hence at least two. The price is
+at least 1+2+2+2=7, again a contradiction. This exhausts t and proves the
+minimum six. The proof requires no width bound or special dirty input.
+
+## Separate finite certificate
+
+Represent rows by a three-by-four matrix of coefficients of (a,b,c,p).
+The start is [I|0] and the target is [I|(2,1,1)]. The twelve cheap generators
+include all three nonzero coefficients on each cheap gate type, so the
+alphabet is closed under inversion.
+
+The verifier enumerates the complete radius-two ball about the start and
+radius-three ball about the target. They contain 99 and 613 matrices and
+have empty intersection. A word of length at most five has a split with
+prefix length at most two and suffix length at most three. Its split matrix
+would lie in both balls. Price-100 gates cannot occur in a cheaper word.
+The six-gate word supplies the matching upper certificate.
+
+This finite computation independently corroborates the written lower bound
+after the coefficient-matrix reduction. The result is an abstract tariff,
+not a physical implementation, supplier or multiplication theorem.

research/z4-directed-cycle-fanout/README.md

@@ -0,0 +1,104 @@
+# Exact nonunit dirty fanout on a cheap directed cycle
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For demand `(2,1,1)` over `Z/4`, the exact price is **six** when source
+insertion into row zero and the directed ADD cycle `0 -> 1 -> 2 -> 0`
+cost one, while all other source insertions and ADD directions cost 100.
+Every nonzero coefficient has its gate's price. All three inputs are
+arbitrary dirty rows; the disjoint source is preserved. There is no workspace.
+
+This is a **scoped written proof with an exact finite certificate**, answering
+the concrete cheap-cycle case suggested in Open next question 1 of
+[lee-phys, PR #5163](https://github.com/CrocSwap/integer-mult-bounds/pull/5163).
+That predecessor determines destination-only prices and leaves independent
+directed prices open. Its result is cited, rather than replayed as the
+contribution. The new chronological word is
+
+```text
+E_21(-1), E_10(-1), P_0(1), E_10(1), P_0(1), E_21(1)
+(a,b,c,p) -> (a+2p,b+p,c+p,p).
+```
+
+Here `E_ij(c)` adds `c A_j` into `A_i`, and `P_i(c)` adds `c p` into `A_i`.
+Every gate costs one. The word uses a path inside the cycle; the third cheap
+edge remains available to competitors. [PROOF.md](PROOF.md) proves the
+endpoint at every positive width and excludes every cheaper word, with
+arbitrary repetitions, interleavings and nonzero coefficients. This supplies
+one exactly solved independent-edge instance, not an arbitrary-price formula.
+No new kappa, physical caller or selected-frontier change is claimed.
+
+## Evidence and reproduction
+
+Complete cheap-word balls of radii two and three contain 99 and 613 literal
+three-by-four coefficient matrices, and are disjoint. Every word of length
+at most five would give an intersection, since all inverses are available.
+A separate scalar interpreter checks all 256 four-scalar inputs and their
+inverse executions. Nineteen controls cover six gate deletions, six sign
+changes, invalid gates and capacity limits. All nine directed gate types
+have their prices checked. Each successful invocation prints a generated
+receipt bound to all package-file SHA256 hashes. No receipt is handwritten.
+
+From the repository root, using CPython 3.12 and only its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/z4-directed-cycle-fanout/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/z4-directed-cycle-fanout/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/z4-directed-cycle-fanout
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/z4-directed-cycle-fanout --check-source-history
+```
+
+Any CPython 3.12 installation can replace the local path. Expected markers
+are `PASS_Z4_DIRECTED_CYCLE_FANOUT`, `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_RESEARCH_COMMIT_BYTES`. Normal and optimized runs retain all checks.
+
+## Sources and scope
+
+Scientific base is canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`,
+priority revision eight. Selected-source orientation passed with
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; it was metadata orientation.
+TASK.json changes the historical `bit-helper-contract` card to this algebraic
+side question. There is no G20 implementation claim.
+
+Credit lee-phys #5163 for the question, destination-price theorem and unit-arrival
+argument; Krzysztof Wójt [#5045](https://github.com/CrocSwap/integer-mult-bounds/pull/5045)
+for nonunit source-count classification and repeated-insertion words; and
+Ross Richardson [#3121](https://github.com/CrocSwap/integer-mult-bounds/pull/3121)
+and #3063 for edge-priced forest synthesis and dirt restoration. The new word
+adapts established child-first preparation to separated source insertions.
+Nick Petalas #4916, Cinna Davis #1944/#1968, Anthony #774, Oscar Fennell #759
+and Tekalign #3130 retain the earlier lineage. Classical matrix identities
+are not claimed as new methods. Predecessor proof text is provenance-pinned;
+no predecessor executable is imported or scientifically replayed.
+
+Entry overlap covered 310 open PRs and 5,456 Discussion records in the reported
+cache, live handoff and fanout threads, account submissions, all-main README
+terms and distinctive merged-PR searches. Only one recent account target came
+from #5163; its equal-nonunit question differs from this unit-containing
+independently priced instance. Unpublished work and arbitrary diffs remain
+outside novelty coverage.
+
+Independent human and formal proof-kernel review are unclaimed. Physical
+coefficient preparation, native frames, movement, precision, tape, storage and
+the full supplier invoice remain unpriced. No multiplication theorem, Lean,
+Docker or selected scientific cold replay is supplied.
+
+## Implementation limits
+
+There is no recursion, external process, network or output file. Words have
+at most 64 gates; matrices have twelve residues; search radius is at most
+three with a checked 1,000-state capacity. Functions have fewer than sixty
+lines. Python managed allocation is a deviation from Power of Ten's fixed
+allocation rule, confined to these bounded matrices and searches. The
+compensating controls reject larger radii and words. A larger search needs
+separately reviewed capacities. Warning-strict normal and optimized checks
+exercise the limits. No shared implementation is changed.
+
+## Open next questions
+
+1. Determine the full directed-price envelope for this demand. Start with
+   directional subset cuts and a complete Pareto search. The present proof
+   solves one price matrix and does not enumerate that envelope.
+2. Price one physical realization before using the word in a supplier.
+   Specify coefficient access, routing, native frames and restoration.
+   Those complete physical prices are missing from the abstract model.

research/z4-directed-cycle-fanout/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/local-ring-row-fanout/README.md",
+      "usage": "provenance",
+      "git_blob": "a65ecdb615300c6b4357eadadb52b46cfbc363ba",
+      "sha256": "4f167d526d889089717b9ba273bc7d048efe4ec1e02cdd91456543e7fc9703fb"
+    },
+    {
+      "path": "research/two-row-nonunit-fanout/README.md",
+      "usage": "provenance",
+      "git_blob": "ea27d3919102a2e66ab4d3ed9170edafee633a06",
+      "sha256": "8aba08fc4a0c049ffaa20f12ca96bbfc582f853ed063a2f694a6bf853c637313"
+    },
+    {
+      "path": "research/dirty-anchor-edge-tariffs/README.md",
+      "usage": "provenance",
+      "git_blob": "16aa73e36b791fd4c025011123b8101dd4a1c2d6",
+      "sha256": "dae5277016949f17bc55191e34a5f9470475b94ed679c843217973711ce2a341"
+    }
+  ]
+}

research/z4-directed-cycle-fanout/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "bit-helper-contract",
+    "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "research/g20-helper-split/README.md",
+      "research/g20-conjugation-admission/README.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "G20",
+      "helper split",
+      "5679",
+      "5708",
+      "independent target"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact price six for Z/4 demand (2,1,1), three dirty rows, one preserved source, unit-price directed cycle and P0, all other gate types priced 100.",
+  "scope_change_reason": "Take explicit cheap-cycle Open next question 1 of lee-phys PR5163 as an algebraic side result; no G20 word or supplier admission is claimed.",
+  "bottleneck_link": "Nonunit demands can invalidate unit-forest prices. One exactly solved directed instance supplies a small benchmark for routing and restoration accounting, without a supplier claim.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified original exact minimum or a documented search failure.",
+  "outcome": "completed",
+  "evidence": "Six-call all-cheap word; written all-width lower bound; disjoint complete balls of sizes 99 and 613; 256 literal forward/inverse cases; 19 controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the complete directed-price envelope for demand (2,1,1) over Z/4?",
+      "why_it_matters": "One price matrix does not classify independent edge tariffs.",
+      "first_step": "Retain directed subset cuts and enumerate Pareto word counts.",
+      "blocked_by": "No all-price lower-bound classification is supplied."
+    },
+    {
+      "question": "Can a physical caller realize this abstract six-call word at favorable complete prices?",
+      "why_it_matters": "An abstract tariff is not a supplier improvement.",
+      "first_step": "Specify source access, routing, coefficient preparation, native frames and restoration.",
+      "blocked_by": "No physical caller and price contract is supplied."
+    }
+  ]
+}

research/z4-directed-cycle-fanout/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Literal endpoint and inverse; complete radius-two/radius-three exclusion; all scalar dirty inputs; omission, sign, invalid-input and capacity controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Literal endpoint and inverse; complete radius-two/radius-three exclusion; all scalar dirty inputs; omission, sign, invalid-input and capacity controls."
+    }
+  ]
+}