DONE: exact two-row nonunit dirty-fanout tariff (#5045)

[krzysztofwojt]

DONE / scoped proof and exact finite corroboration / 2026-10-23 / priority revision 7. Claim released.

PR #5045, exact head 8639d7b6348d9b09683e71d74afcceedf2d4bdc0, supplies a five-term exact tariff for two dirty output rows whose demand coefficients generate comparable principal left ideals. This includes every pair over Z/p^k, zero demands and suitable noncommutative-ring pairs. The proof permits arbitrary positive, stationary, coefficient-independent prices and arbitrary straight-line interleavings.

The attaining construction chooses between a second source insertion and reversible row mixing. For Z/4 demands (2,1), source prices (100,1000) and ADD prices (1,1), mixing costs 104, while repeated insertion costs 202. The predecessor's optimum-four example remains credited calibration. No new κ or physical supplier is claimed.

Public artifact: research/two-row-nonunit-fanout/, including PROOF.md, constructive code, the separate exact shortest-path oracle, source pins and generated receipt.

Evidence: 17,313 optimum comparisons in 522 exact modular graph searches, 2,591 attaining words, 7,773 coefficient-column/inverse checks and 4,800 literal dirty-state/inverse checks. Registered normal/optimized replay, committed-byte/source-history preflight, export integrity and read-only Git-free normal/optimized replay pass. Seven disposable-export corruption controls reject, including three semantic mutations with rebound source hashes. Hosted CI is separate; see the PR's current checks.

Smallest useful next tasks: a structural criterion for incomparable demands, starting with (2,3) over Z/6; a three-row nonunit word/cut comparison; or an actual caller's complete coefficient-independent tariff matrix. These require new results. More rows, incomparable demand ideals, physical framing/routing/precision/tape costs and compiler/outer admission are not established here. The universal conclusion rests on the written proof, with no independent human or proof-kernel acceptance claimed.

Credit Nick Petalas #4916, Ross Richardson #3121/#3063, Cinna Davis #1944/#1968, Anthony #774, Oscar Fennell #759, Tekalign #3130 and the retained lineage. Prepared by Krzysztof Wójt with substantial OpenAI Codex assistance; Apache-2.0. Selected κ remains 0.00302015.

Original scoped claim, retained for provenance

CLAIM — exact two-row nonunit dirty-fanout tariff; no new κ.

I take the structural nonunit-demand question left by Nick Petalas's #4916 handoff. The published Z/4 example already has optimum four and will be a credited calibration, not a new result.

Question: for two arbitrary dirty output rows and one preserved, disjoint common source, what is the exact minimum price when the two demand coefficients generate comparable principal left ideals? This includes every pair over Z/p^k. Retain precisely the predecessor's coefficient-independent positive source/ADD tariffs, arbitrary straight-line interleavings and full restoration of both original dirt coefficients. No extra workspace, free basis change, intermediate observer or physical price is introduced.

Method and bounded domain: classify words by source-insertion counts, prove the necessary directional-ADD counts, and exhibit attaining words. The intended result is a finite cost envelope separating one source insertion with reversible row mixing from two insertions at the same row. Check it independently by exact shortest paths on complete small modular affine-state spaces, with literal dirty-state and inverse controls. Zero demands and left-versus-right coefficient order will be explicit boundary cases. Universal conclusions must follow from the written proof, not the finite searches.

Value/scope decision: this answers a named unresolved structural tariff question rather than rerunning the unit theorem or its existing Z/4 example. It is a scoped algebraic interface result; an actual caller, coefficient-dependent physical costs, more than two rows, incomparable demand ideals, compiler/outer admission and a new κ remain outside the claim. Stop after one exact theorem or a discriminating counterexample. The bit-helper-contract card is explicitly changed to this handoff's algebraic contract.

Base: canonical main f259dabc7d70e0db8d6d36bfda888f008bbfecc1, re-fetched unchanged before this claim, priority revision 7; selected κ remains 60403/20000000. Predecessor #4916: 459a1d9984e8c5bf09257a409863e63282c282e6, retained under research/unit-ring-dirty-fanout/. Credit Nick Petalas, Ross Richardson #3121/#3063, Cinna Davis #1944/#1968, Anthony #774, Oscar Fennell #759, Tekalign #3130 and their retained lineage.

Overlap: complete cached remote pagination (320 open PRs and 4,130 Discussion records, refreshed 06:48–06:49 UTC), all 6,710 main README/TASK notes, distinctive nonunit/fanout searches, the live merged #4916 head and current handoffs/open PRs were checked. No competing structural two-row nonunit result was identified in that coverage; arbitrary diffs and unpublished work are not covered. Expected artifact: one isolated package with proof, constructive tariff routine and independently implemented exact finite checker. Evidence is LOCAL-ONLY until publication. Prepared by Krzysztof Wójt with substantial OpenAI Codex assistance.

Claim expires: 2026-10-23T08:55:00Z.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"bit-helper-contract","scope":"Exact two-row nonunit dirty-fanout tariff for comparable demand left ideals; all-price proof, attaining words and independent bounded shortest-path corroboration; no new kappa","base":"f259dabc7d70e0db8d6d36bfda888f008bbfecc1","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/5045"}

[lee-phys]

DONE — PR #5089, exact head ba325c0b94bc69d2a0d264bec581899f220d4613. Claim released.

This resolves #5045 Open next question 1 in the residue-ring two-row contract. For (2,3) over Z/6 and arbitrary positive stationary coefficient-independent prices, the optimum is

min(mu0+mu1, 2mu0+2c1, 2mu1+2c0,
    mu0+2c0+2c1, mu1+2c0+2c1).

Five explicit words attain the five terms, and their count vectors are exactly the Pareto frontier. The new coefficient-selection lemma chooses beta=x-a*y generating (x,y) using CRT, then writes y=r*beta. It extends #5045's piecewise two-row tariff to every demand pair over every Z/n, n >= 2, including nonunit common generators. The source-count lower bound and directional return lemma remain credited to Krzysztof Wójt's #5045 and are restated in the self-contained proof.

Public artifact: research/z6-incomparable-fanout/. The five-file package contains the proof, exact constructor, separate primitive-state Dijkstra oracle, provenance pins and normal/optimized replay hook.

Exact evidence: 119 full-graph Dijkstra runs and 3,654 optimum comparisons; 9,830 ordered CRT checks; 24,575 candidate words; 147,450 forward/inverse basis checks; 2,160 literal Z/6 checks; 16 built-in controls and three rejected disposable semantic mutations. Registered normal/optimized replay, committed-byte/source checks, official export integrity and read-only Git-free normal/optimized replay pass, with all six exported files unchanged. Full source-history ancestry checking was not run in the shallow checkout. The universal conclusion rests on the written proof, not the finite searches; no independent human or proof-kernel acceptance is claimed.

Hosted CI passed both planning and the registered package replay at this exact head in run 39926839937. This is replay evidence, not mathematical acceptance.

Scientific base: latest canonical main 81e9bd69e4a5b00ba9c713a1620e36d576d5522e, unchanged at submission refresh. Complete reported remote pagination covered 307 open PRs (08:39 UTC) and 4,212 Discussion records (08:41 UTC), supplemented by targeted all-state searches and this thread. No resolving successor was found within that coverage. Local note coverage is sparse; arbitrary diffs and unpublished work are not exhaustively covered.

Remaining questions are the one-insertion orbit over other rings, three-row nonunit sharing and one actual physical caller with complete prices. No physical supplier, compiler/outer admission, selected-frontier change or new κ is claimed. Credit Krzysztof Wójt #5045, Nick Petalas #4916, Ross Richardson #3121/#3063, Cinna Davis #1944/#1968, Anthony #774, Oscar Fennell #759, Tekalign #3130 and the retained lineage. Prepared by lee-phys with substantial OpenAI Codex assistance; Apache-2.0.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"bit-helper-contract","scope":"Exact all-price two-row dirty-fanout tariff for (2,3) over Z/6 and all demand pairs over every Z/n, via CRT coefficient selection","base":"81e9bd69e4a5b00ba9c713a1620e36d576d5522e","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/5089"}

[lee-phys]

DONE — PR #5139, exact contribution head ec44e8bec68b49a1ba7adaac8a0bba0192bd638c. Claim released. This completes the finite-commutative-ring follow-up to #5089; the earlier #5089 DONE remains separate.

Result. For nonzero two-row demand over any finite commutative unital ring, exactly one nonzero source insertion is feasible iff the generated demand ideal is principal. Either insertion row works using at most four row additions. Necessity is ideal invariance under invertible row gates; sufficiency uses CRT/stable reduction in the annihilator quotient of an ideal generator. The zero-demand exception is explicit. Combining this with Krzysztof Wójt's #5045 source-count lower bound yields the exact tariff at every positive stationary coefficient-independent price, with attaining words and full dirt restoration.

For the eight-element ring F2[epsilon,eta]/(epsilon^2,epsilon eta,eta^2), demand (epsilon,eta) generates a nonprincipal ideal. Its exact Pareto frontier consists of (1,1,0,0), (2,0,0,2) and (0,2,2,0) in (P0,P1,E0,E1) order. Thus OPT is min(mu0+mu1,2mu0+2c1,2mu1+2c0). At prices (100,1000,1,1), OPT=202, while the unavailable single-insertion term would incorrectly predict 104.

Public artifact: five-file proof and verifier package.

Evidence: nine finite rings, 1,761 demands (102 nonprincipal), 3,522 row-specific column-orbit comparisons, 3,318 witnesses, 8,601 words, 51,606 forward/inverse basis checks and 3,072 literal scalar checks. Forty-five complete-graph Dijkstra runs compare 2,348 optima; all Bellman inequalities and tight parent paths are checked. Eleven built-in controls and three disposable semantic mutations pass. Registered normal/optimized replay, metadata/provenance checks, committed-byte preflight, official export integrity and read-only Git-free normal/optimized replay pass; all six exported files are unchanged. Full source-history ancestry checking was not run in the shallow checkout. Hosted CI also passes at this exact head: run 39941031342, planning in 4m45s and the focused normal/optimized package replay in 1m19s. Main advanced to a5df48c during publication; the task guidance and both predecessor pins remain unchanged.

The universal claim rests on the written proof. This is author-checked, AI-assisted work, not independent human or proof-kernel acceptance. No native caller, supplier or new kappa follows. Nonsemilocal-ring orbit obstructions, three-row tariffs and a concrete caller's physical costs remain distinct open questions and are unreserved.

Credit lee-phys #5089 for the residue-ring result and handoff; Krzysztof Wójt #5045 for the lower-bound classification, return lemma and standard constructions; Nick Petalas #4916 for the ring-valued contract; Ross Richardson, Cinna Davis, Anthony, Oscar Fennell, Tekalign and the retained lineage. CRT and stable reduction are classical. Prepared by lee-phys with substantial OpenAI Codex assistance; Apache-2.0.

Coordination note: the original claim was posted at 10:32 UTC; its displayed 10:40 timestamp was a transcription error, corrected by this completion update.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"bit-helper-contract","scope":"Principal-ideal criterion and exact all-positive-price two-row dirty-fanout tariff over finite commutative unital rings","base":"20a1e31bc6009b9b3f4d084bbaadc6350e34fcba","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/5139"}

[lee-phys]

DONE — PR #5163, exact contribution head cdd7714c20352f7106f005066c3ed65534e98516. The scoped claim is complete and released.

For Z/4 demand (2,1,1), the exact all-positive destination-priced tariff has eight indispensable terms, with all eight attaining count vectors forming the aggregate Pareto frontier. Source prices (1,9,9) and unit ADD prices give optimum 6; (100,1000,1000) and unit ADD prices give 106.

The proof extends to any row count over any commutative local ring with at least one unit demand; zero-demand temporary recipients are included. An incoming row cannot receive exactly one nonzero ADD while restoring arbitrary dirt. Locality then forces a unit insertion somewhere; a nonunit-demand recipient must pay another insertion or at least two incoming ADDs. Explicit echo/repeated/mixing words match the resulting formula for all positive stationary coefficient-independent destination prices. A Z/6 example has exact optimum 24 versus the invalid extension's 32, demonstrating the locality boundary.

Public artifact: five-file proof/verifier package. Six local rings, 2,011 demand-list fixtures, 6,033 price instances, 25,179 words, 213,744 formal-column forward/inverse executions and 6,688 literal executions pass. Sixteen separately implemented bidirectional Dijkstra queries certify unrestricted three-row Z/4 optima, settling 154,814 entries across both directions and queries; there is no depth cutoff or formula pruning. This is not an exhaustive enumeration of the entire graph. Fifteen built-in controls and three disposable optimized-script mutations pass. Registered normal/optimized replay, metadata/pins, committed bytes, official export integrity and read-only Git-free normal/optimized replay all pass, with all six exported files unchanged.

Both hosted checks passed at exact contribution head cdd7714c20352f7106f005066c3ed65534e98516 in Registered research packages run 39945882387: planning in 4m37s and focused package replay in 1m25s. Run metadata confirms conclusion success and the exact head. The replay runs both registered normal and optimized commands. Execution success is separate from independent acceptance of the universal written proof.

Scientific base: freshly fetched canonical main a5df48c55ea806d7952b65acc9c76d878ff09b13, unchanged at the submission refresh; priority revision 7. Entry pagination covered 312 open PRs and 4,318 Discussion records. Submission targeted all-state PR searches and live #5030/#1166 reads found no resolving successor within that coverage. Sparse historical notes, arbitrary diffs and unpublished work were not exhaustively searched.

This closes the stated destination-price family of #5045/#5139's three-row question. Independently priced directed edges, nonzero all-nonunit demands and a complete physical caller remain open and unreserved. The universal claim rests on the written proof; no independent human or proof-kernel acceptance, physical supplier or new kappa is claimed. Optional full source-history checking was not run in the shallow checkout; all scientific provenance pins are at the main base, and pending #5139 is not an executable/proof dependency.

Credit Krzysztof Wójt #5045 for the source-count method and repeated/mixing words; Nick Petalas #4916 for the ring-valued contract; Ross Richardson #3063/#3121 for destination/edge tariffs and dirt restoration; Cinna Davis, Anthony, Oscar Fennell, Tekalign and the retained lineage. Prepared by lee-phys with substantial OpenAI Codex assistance; no subagents or independent reviewers. Apache-2.0.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"bit-helper-contract","scope":"Exact destination-priced dirty-fanout tariffs over commutative local rings with a unit demand; eight-term Z/4 (2,1,1) frontier","base":"a5df48c55ea806d7952b65acc9c76d878ff09b13","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/5163"}

[lee-phys]

DONE — PR #5259, contribution head d2a7d88f011ca9c520333da8d4e03f1f22d23e91. This scoped investigation is complete and the advisory claim is released.

The destination-row tariff for (e,h,e+h) over F2[e,h]/(e,h)^2 is exactly the nineteen-term envelope in the proof package. All nineteen aggregate count vectors are attained, form the complete Pareto frontier, and are uniquely exposed by some strictly positive prices. The proof extends to every commutative unital ring for a zero-sum triple generating a nonprincipal ideal. It covers arbitrary finite interleavings, feedback and cancelling unit insertions under the stated three-dirty-row/one-preserved-source contract. At mu=(1,9,9), c=(1,1,1), the requested instance costs exactly six.

The new step is the exhaustive two-insertion-row surcharge, using ideal invariance and the incoming-row return argument, plus five matching word families. Credit lee-phys #5139/#5163, Nick Petalas #5208/#4916, Krzysztof Wojt #5045, Ross Richardson #3063/#3121 and the retained fanout lineage. Prepared by lee-phys with substantial OpenAI Codex assistance; no subagents or independent reviewers.

Normal and optimized direct/registered checks pass with identical output. Four rings cover 102 valid demand triples, 1,938 words, 15,504 formal column checks and 155,648 literal scalar checks. Seven independently implemented unrestricted packed-state shortest paths agree with the formula; all returned words are replayed and charged by the primary interpreter. Eight controls and three disposable optimized-mode mutations distinguish missing hypotheses, corrupted dirt restoration and incorrect pricing. Metadata/pins, committed bytes, official export integrity and both read-only Git-free export modes pass, with all six exported files unchanged. The optional full-history preflight was not run in this shallow checkout; all provenance pins refer to the direct main parent.

Hosted CI passed for this exact head: Registered research packages run 39970918113. Both planning and the focused registered replay succeeded; the replay executes the normal and optimized warning-strict commands. Run metadata confirms completed status, success and the matching head SHA.

Entry and submission overlap refreshes found no resolving successor. Canonical main remains the pinned base ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7. The prior survey covered 311 open PRs and 4,490 Discussion records; targeted all-state fanout/zero-sum searches and live #5030/#1166 delta reads were refreshed before publication. Sparse historical notes, arbitrary diffs and unpublished work are not exhaustive novelty coverage.

The universal theorem rests on the written proof; finite verification and hosted execution are separate from independent human or proof-kernel acceptance. Directed-edge prices, additional helper rows and physical supplier accounting remain outside scope. No new kappa or selected-frontier change is claimed. Open next questions: the principal-ideal Boolean triple (3,5,6) (the displayed cost-16 word is only an upper bound there), independent directed-edge tariffs, and non-zero-sum demands. These follow-ups are unreserved.

Reproduce from the repository root with Python 3.12:

python3.12 -B scripts/research_package.py --package research/square-zero-triple-fanout

[lee-phys]

DONE: PR #5304 proves the exact 22-term destination-row tariff for (110,101,011) over F_2^3, settling Open next question 1 of #5259. Contribution head: c8bf34c359b3a12f112078f0072b4ecc7a942109; self-contained proof and verifier.

The new one-insertion branch is U_i=mu_i+2(c_0+c_1+c_2). Ideal invariance forces the inserted coefficient to generate the whole demand ideal, while no individual demand does. Therefore even the insertion row needs incoming ADDs, and dirt restoration makes every row require at least two. The previous seven-gate Boolean witness attains this bound. Combining the three U vectors with #5259's nineteen multi-insertion vectors gives the complete Pareto frontier; every vector is uniquely optimal at some strictly positive prices. The old cost-16 upper bound is now exact. Uniform prices simplify to min(3mu,mu+6c).

The written proof extends to every commutative unital Boolean ring, even infinite ones, when the demands sum to zero and their principal ideals are pairwise incomparable. Ali Romman's #5266 and new #5300 already settle insertion count in broader ring classes; they explicitly leave total tariffs open and retain credit. The new contribution concerns the complete price envelope.

Local evidence: 456 demand triples, 10,032 constructed words, 80,256 formal forward/inverse column checks, 180,224 literal input checks, all 22 strict price exposures, eleven controls and seven independent packed-state shortest-path cases. Normal and optimized checks, three deliberate failure mutations, registered replay, metadata, committed bytes, official export integrity and read-only Git-free replay all pass. Hosted CI also completed successfully for this exact head, including planning and the registered normal/optimized replay. Independent human review and proof-kernel acceptance remain unclaimed.

Canonical main remained ff3cc58e370d0f678e529246f8c73e8094e18fcf at the submission refresh. Entry and submission checks found no competing same-tariff result or active claim in the inspected PR/Discussion records. Sparse local notes, arbitrary historical diffs and unpublished work remain coverage limits. This completes the claim posted here at 16:29 UTC; no continuation is reserved.

Next questions are independently directed-edge prices and the non-zero-sum Boolean demand (1,2,4), with concrete first steps and blockers in TASK.json. They are suggested questions, not novelty certificates. Credit #5259/#5139/#5163, Ali Romman #5266/#5300, Nick Petalas #5208/#4916, Krzysztof Wojt #5045, Ross Richardson #3063/#3121 and the retained earlier fanout lineage. Prepared by lee-phys with substantial OpenAI Codex assistance; no subagents, physical supplier admission or new kappa.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"boolean-triple-fanout","scope":"Exact 22-term destination-row tariff and Pareto frontier for (110,101,011) over F2^3 and zero-sum incomparable triples over Boolean rings","base":"ff3cc58e370d0f678e529246f8c73e8094e18fcf","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/5304"}