Skip to content

Prove exact twenty-two-term tariffs for Boolean fanout triples - #5304

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

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

Conversation

@lee-phys

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

Copy link
Copy Markdown

The Boolean-product demand (110,101,011) now has an exact 22-term tariff for every strictly positive destination-row price vector, with matching constructions and an all-word lower bound. This resolves Open next question 1 of #5259. Its one-insertion cost-16 example was previously only an upper bound; it is now proved optimal at those prices.

With insertion price mu_i and ADD price c_i for the receiving row, write {i,j,k}={0,1,2}:

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)
U_i = mu_i + 2(c_0+c_1+c_2)
OPT = min(D,T_0,T_1,T_2,B_0,B_1,B_2,U_0,U_1,U_2).

The new branch proves that a single insertion at row i requires at least two ADDs into every row: its coefficient must generate the full demand ideal, while no individual target does, and restoration rules out exactly one incoming ADD. A three-ADD suffix and its inverse attain those six additions. The nineteen multi-insertion vectors from #5259 remain necessary; the three U vectors complete the Pareto frontier. Explicit positive prices expose every vector uniquely.

The self-contained proof extends to every commutative unital Boolean ring, including infinite rings and proper demand ideals, provided the demands sum to zero and their principal ideals are pairwise incomparable. For uniform prices it simplifies to min(3mu,mu+6c). Exactly three arbitrary dirty rows and one preserved disjoint source are allowed; coefficients and directed pairs are unrestricted, but prices depend only on receiving row and operation type.

Only five new files in research/boolean-triple-fanout/ are changed. The original task card, changed donor-assigned scope, source attribution, mathematical proof, bounded standard-library verifier and next questions are included. No selected-frontier file is changed and no new kappa or physical supplier admission is claimed.

Validation at contribution head c8bf34c359b3a12f112078f0072b4ecc7a942109:

  • CPython 3.12.13 normal and optimized isolated, warning-strict checks agree. Three Boolean rings cover 456 demand triples, 10,032 words, 80,256 formal forward/inverse column checks and 180,224 literal scalar checks; all 22 count vectors are strictly exposed, with eleven boundary controls.
  • A separate packed-state bidirectional Dijkstra implementation allows all 63 nonzero primitives, all original dirt columns and arbitrary interleavings, without a length cutoff or formula-based pruning. Seven exact-price cases cover all six families plus rational prices; they settle 314,361 states in total and return independently replayed and charged words. This is not an enumeration of the entire affine graph.
  • Three disposable optimized-mode mutations fail: undercharging U, omitting its dirt preparation and ignoring heterogeneous oracle prices.
  • Both registered commands, metadata/source pins, exact committed bytes and the official export integrity check pass. Both warning-strict modes also pass from a read-only export outside Git with PATH=/nonexistent, identical output and all six exported files unchanged. The optional full-history preflight was not run in this shallow checkout; every declared Git provenance pin refers to the direct main parent.

Reproduce:

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

Base: freshly fetched canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7, unchanged at the 16:40 UTC submission refresh. Entry checks used complete snapshots of 347 open PRs and 4,548 Discussion records, then live all-state fanout PR searches and board/#1166/#5030 updates. The submission refresh read the new #5300 as well: it extends source-insertion count to finite associative rings and explicitly leaves total tariffs open. #5266/#5269 likewise do not resolve this price question. No competing same-tariff result or active claim appeared in the inspected records. Sparse local notes, arbitrary historical diffs and unpublished work remain coverage limits. Canonical investigation.

Credit lee-phys #5259 for the existing nineteen vectors, words, Boolean witness and adapted verifier infrastructure; Ali Romman #5266/#5300 for the many-row insertion-count results; #5139/#5163, Nick Petalas #5208/#4916, Krzysztof Wojt #5045, Ross Richardson #3063/#3121 and the earlier fanout lineage. The pending predecessor is precisely cited and its needed arguments/code are reproduced or adapted locally; replay does not fetch or import its unmerged Git objects. Prepared by lee-phys with substantial OpenAI Codex assistance; no subagents or independent reviewers were used. Apache-2.0.

The universal statement rests on the written proof; finite checks do not provide independent human review or proof-kernel acceptance. Independently directed-edge prices, extra helpers, non-Boolean carriers and physical supplier accounting are outside this contract.

Hosted CI passed for this exact contribution head: Registered research packages run 39989829494. Planning and the focused replay completed successfully; the latter executes both registered normal and optimized commands. Run metadata confirms completed, success and head c8bf34c359b3a12f112078f0072b4ecc7a942109. No review submissions or conversation comments were present at the final check.

@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