Skip to content

Prove exact 25-term tariffs for orthogonal Boolean fanout triples - #5514

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

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

Conversation

@lee-phys

Copy link
Copy Markdown

Demand (1,2,4) over F_2^3 is outside the zero-sum tariff theorem in #5304. This contribution resolves its Open next question 2: with three arbitrary dirty rows, one preserved source and arbitrary positive destination-row prices, the exact optimum has 25 indispensable linear terms, each with an attaining word. The proof extends to three nonzero pairwise orthogonal demands over any commutative unital Boolean ring.

The new one-insertion argument cuts at the sole source call. Both the suffix and inverse prefix must transport the same generator column to the demand, and each needs at least four ADDs. This gives the sharp bill mu_i + 2 sum(c) + 2 min(c); the extra two ADDs may use any row, independently of the insertion row. In the multi-insertion classification, the former two-fixed-parent branch is impossible because the third demand lies outside the other two demands' ideal. New non-zero-sum words attain the remaining branches. Uniform prices simplify to min(3mu, mu+8c), compared with the zero-sum predecessor's min(3mu, mu+6c).

Only research/orthogonal-boolean-fanout/ is added (five files): self-contained proof, standard-library verifier, exact source pins and registered replay metadata. This is an exact price envelope, not a claim to enumerate every unexposed Pareto vector. It does not change the selected frontier or establish a physical supplier/new kappa.

Validation on Python 3.12:

  • Registered normal and optimized warning-strict replays pass with identical evidence: 456 demands, 11,400 constructed words, 91,200 formal forward/inverse column checks, 204,800 literal input checks, all 25 strict price exposures and ten controls.
  • 81 independent weighted source-column Dijkstra queries confirm the new four-ADD bound. Five unrestricted full dirt-state shortest paths settle 90,347 states; exact optima are 3, 6, 6, 14 and 41/15. The U branches use column-search corroboration plus full endpoint replay; those five full-state queries do not cover U-optimal prices.
  • Three disposable optimized-mode mutations reject underpricing the single-insertion branch, omitting a suffix gate and forcing the cheapest extra ADD destination to equal the insertion root.
  • Package metadata/pins, committed-byte check, official export integrity and a read-only Git-free exported replay pass. Full-history ancestry checking was not run in the shallow checkout; every Git provenance pin is at the direct main parent. Hosted CI is pending.

Reproduce:

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

Scientific base: canonical main 32890bc5de034ab8fc93ac88ead7279a6a416d04, priority revision 7. Contribution commit: 377af21a21d7e8bf4db682ece724915f83703044. Entry overlap refresh covered 371 open PRs and 4,779 Discussion records with complete pagination, plus all-state targeted PR searches and current #1166/#5030 reads. No resolving same-scope result or active claim was found; arbitrary historical diffs and unpublished work are outside exhaustive coverage. Completion refresh: canonical main remained unchanged; 371 open PRs at 2026-10-25T05:45:52.718514+00:00 and 4779 Discussion records at 2026-10-25T05:48:23.184729+00:00, both completely paginated. No new matching result or claim appeared. Publication delta check at 2026-10-25 05:52 UTC confirmed the same canonical main, no existing PR for this branch and no new #1166/#5030 comment since the complete snapshot.

Credit lee-phys #5304/#5259 for adapted verifier infrastructure and the support framework; Ali Romman #5266/#5310 for insertion feasibility; #5139/#5163, 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 or independent reviewers. Apache-2.0. General Boolean-ring and arbitrary-real-price claims rest on the written proof; no independent human or proof-kernel acceptance is claimed.

@Mister-Meeseeks
Mister-Meeseeks merged commit d99b379 into CrocSwap:main Oct 25, 2026
2 checks passed
Mister-Meeseeks pushed a commit that referenced this pull request Oct 28, 2026
Decide every eight-ADD one-insertion count vector for the PR #5514 demand
over F2^3 by enumerating all ADD-only words with at most four gates. Two
extra ADDs may sit in the insertion row and any other row, never in both
non-insertion rows. Six new unexposed vectors join the 25 price-envelope
vectors to give a 31-vector aggregate frontier.
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