Skip to content

Prove exact nineteen-term tariffs for nonprincipal zero-sum triples - #5259

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
lee-phys:codex/square-zero-triple-fanout
Oct 23, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
lee-phys:codex/square-zero-triple-fanout

Conversation

@lee-phys

@lee-phys lee-phys commented Oct 23, 2026 •

Copy link
Copy Markdown

The previously open demand (e,h,e+h) over F2[e,h]/(e,h)^2 now has an exact tariff for every strictly positive destination-row price vector. This package proves the all-word lower bound, gives every matching construction, and identifies all 19 indispensable aggregate count vectors. It resolves the unequal all-nonunit example left by #5163 and #5208.

The theorem extends to any commutative unital ring and any triple whose sum is zero and whose generated ideal is nonprincipal. Finiteness and locality are unnecessary. There are exactly three arbitrary dirty rows and one preserved disjoint source; all original dirt must return. Insertion into row i costs mu_i; every ADD into row i costs c_i. Prices are stationary, coefficient-independent complete abstract prices.

For distinct i,j,k, the compact formula is:

D   = mu_0 + mu_1 + mu_2
T_i = 2mu_i + 2c_j + 2c_k
B_k = mu_i + mu_j + 2c_k + min(mu_i,mu_j,2c_i,2c_j,2c_k)
OPT = min(D,T_0,T_1,T_2,B_0,B_1,B_2).

The proof classifies insertion support. A nonprincipal ideal excludes a single insertion. Dirt restoration excludes exactly one incoming ADD per row. In the two-insertion-row case, either an insertion repeats, an insertion row must itself be restored, or the remaining row needs two calls from each unchanged parent. These cases supply the new exhaustive surcharge. Five word families attain the bounds, and explicit positive prices expose every vector uniquely. The argument includes arbitrary feedback, cancellations and interleavings; it never assumes a universal per-edge two-call rule.

At mu=(1,9,9), c=(1,1,1), the requested demand costs exactly 6. A Boolean-product example checks why nonprincipality cannot be omitted: an explicit one-insertion word costs 16 where the inapplicable formula gives 24. The cost-16 witness is only an upper bound for that different instance.

Changes are confined to the five files in research/square-zero-triple-fanout/. The README contains the proof, chronological words, model boundaries and open next questions. Sources retain credit to lee-phys #5139/#5163, Nick Petalas #5208/#4916, Krzysztof Wojt #5045, Ross Richardson #3063/#3121 and the earlier fanout lineage. Prepared by lee-phys with substantial OpenAI Codex assistance; no subagents or independent reviewers were used.

Validation at contribution head d2a7d88f011ca9c520333da8d4e03f1f22d23e91:

  • Normal and optimized isolated, warning-strict Python 3.12 checks pass with identical output, directly and through the registered package runner.
  • Four rings cover 102 valid triples, 1,938 words, 15,504 formal forward/inverse column checks and 155,648 literal scalar checks; all 19 vectors have strict positive-price witnesses, with eight boundary/failure controls.
  • An independently implemented packed-state bidirectional Dijkstra oracle permits every nonzero coefficient and every directed gate, without a length cutoff or formula pruning. Seven exact-price cases agree; returned words are independently replayed and charged. This explores implicit states, not the entire affine graph.
  • Three disposable optimized-mode mutations reject an undercharged insertion count, omitted dirt preparation and ignored heterogeneous oracle prices.
  • Metadata/source pins, exact committed bytes, official export integrity and both read-only Git-free exported replay modes pass. All six exported files remain unchanged. The optional full-history preflight was not run in this shallow checkout; all provenance pins refer to the direct main parent.

Reproduce from the repository root:

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

Base is freshly fetched canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7, unchanged at the submission refresh. The preceding survey covered 311 open PRs and 4,490 Discussion records. Entry and submission checks refreshed targeted all-state PR searches plus #1166/#5030; no resolving successor was found. Arbitrary historical diffs and unpublished work were not exhaustively searched. Canonical investigation.

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.

The universal statement rests on the written proof; finite checks do not provide independent human or proof-kernel acceptance. Independently directed-edge prices, extra helpers and physical supplier accounting are outside this contract. The selected frontier is unchanged and no new kappa is claimed. Next questions concern the principal-ideal Boolean triple, directed-edge prices and demands without the zero-sum relation.

@Mister-Meeseeks
Mister-Meeseeks merged commit 3b785d5 into CrocSwap:main Oct 23, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants