diff --git a/research/boolean-triple-fanout/README.md b/research/boolean-triple-fanout/README.md new file mode 100644 index 0000000000..efa6fe83c9 --- /dev/null +++ b/research/boolean-triple-fanout/README.md @@ -0,0 +1,350 @@ +# Exact tariffs for an incomparable Boolean demand triple + +**Scoped written proof with exact finite corroboration; no new kappa.** +For three arbitrary dirty rows, the demand `((1,1,0),(1,0,1),(0,1,1))` +over `F_2^3` has an exact **twenty-two-term** optimum for every positive +source-insertion price and every positive destination-row ADD price. +All twenty-two aggregate count vectors are attained and indispensable. + +This settles Open next question 1 of lee-phys's +[PR #5259](https://github.com/CrocSwap/integer-mult-bounds/pull/5259), +at `d2a7d88f011ca9c520333da8d4e03f1f22d23e91`. Its nineteen-term theorem +requires a nonprincipal demand ideal and does not apply here. The new step +is the exact one-insertion branch, whose three count vectors complete the +frontier. Ali Romman's +[Discussion #5266](https://github.com/CrocSwap/integer-mult-bounds/discussions/5266) +already proves one-insertion feasibility for principal ideals over finite +commutative rings with any number of rows; it does not price the shortest +restoring word. Both predecessors retain credit. The argument below is +self-contained and extends to arbitrary Boolean rings under stated hypotheses. + +## Contract and optimum + +Let R be a commutative unital Boolean ring, `1 != 0`: every element x satisfies +`x^2=x`. In particular `2x=0`, by expanding `(x+1)^2=x+1`. Exactly three +independent arbitrary dirty rows `a_0,a_1,a_2 in R^w`, w >= 1, and a disjoint +preserved source `p in R^w` are available. A fixed finite word must produce + + A_i = a_i + lambda_i p, i=0,1,2, + +for all input values. The only operations are + + P_i(beta): A_i <- A_i + beta p, price mu_i > 0; + E_ij(alpha): A_i <- A_i + alpha A_j, price c_i > 0, i != j. + +All coefficients and directed row pairs are available. Prices are finite, +stationary, coefficient-independent complete abstract prices; all ADDs into +a given row have the same price. Every original dirt column must return. +There are no extra rows, clearing, observations, adaptive choices or free +basis changes. Any separate inverse execution is charged separately. +Positive prices allow zero-coefficient gates to be deleted. + +**Theorem.** Suppose the three demands sum to zero and their principal ideals +are pairwise incomparable; equivalently, + + lambda_0 + lambda_1 + lambda_2 = 0, + lambda_i not in (lambda_j) for every i != j. + +For distinct i,j,k, define + + 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). + +The exact optimum over all allowed finite words is + + OPT = min(D,T_0,T_1,T_2,B_0,B_1,B_2,U_0,U_1,U_2). + +Expanding the inner minima gives twenty-two linear terms. The value and an +attaining word can be selected with a constant number of comparisons once +the prices and algebraic hypotheses are given. This does not price testing +those hypotheses or physically implementing the gates. + +For the requested `F_2^3` example, encode `(x_0,x_1,x_2)` as +`x_0+2x_1+4x_2`. Addition is XOR, multiplication is AND, identity is 7, +and the demand is `(3,5,6)`. The theorem applies because the three supports +have size two and none contains another. At mu=(10,100,100), c=(1,1,1), +the exact optimum is **16**, attaining the previous upper bound; excluding +the new U terms would incorrectly give 24. +The one-insertion witness for this example was already displayed in #5259. +Its sharp lower bound and the full price envelope are the new conclusions. + +If every mu_i=mu and every c_i=c, the formula simplifies to + + OPT = min(3mu, mu+6c). + +Indeed the B terms are at least `min(3mu,2mu+4c)`. For mu<=3c, +`2mu+4c>=3mu`; for mu>=3c, `2mu+4c>=mu+6c`. Thus three direct +insertions are optimal below the transition mu=3c, and one insertion with +six ADDs is optimal above it; both attain the value at equality. + +## Boolean support algebra + +The hypotheses imply that every demand is nonzero. Define + + a = lambda_0 lambda_1, + b = lambda_0 lambda_2, + c = lambda_1 lambda_2. + +Using `lambda_2=lambda_0+lambda_1` and idempotence gives + + lambda_0=a+b, lambda_1=a+c, lambda_2=b+c, + ab=ac=bc=0. + +For example `ab=lambda_0^2 lambda_1(lambda_0+lambda_1)=0`; +the other products follow by permuting indices. Each of a,b,c is nonzero: +if a=0 then `lambda_0=lambda_0 lambda_2` belongs to `(lambda_2)`, +contradicting incomparability, and the other cases are symmetric. +Conversely, three nonzero pairwise orthogonal idempotents a,b,c give a +triple of this form with incomparable principal ideals: multiplying a +proposed membership by the missing atom yields a nonzero atom equal to zero. + +Set + + g = a+b+c = lambda_0+lambda_1+lambda_0 lambda_1. + +Then `I=(lambda_0,lambda_1,lambda_2)=(g)`: g is a combination of the +lambda_i, and `g lambda_i=lambda_i`. No lambda_i generates I, since that +would contain every other demand. For every pair of distinct indices, + + h_i = g+lambda_i != 0, h_i lambda_j = h_i. + +These identities are the only special algebra needed for the one-insertion construction. +They also allow g to be a proper idempotent, not necessarily the ring identity. +Finiteness and a global decomposition of R into fields are unnecessary. + +## Lower bound for arbitrary words + +Write P_i for the number of nonzero insertions into row i and K_i for the +number of all incoming nonzero ADDs. Prefixes act on the three original dirt +columns by an invertible matrix M: an ADD has its negated-coefficient inverse, +and an insertion does not change M. The all-input requirement forces the +final dirt matrix to be the identity, as seen by testing each original input +column separately. + +**Incoming-row return lemma.** No row receives exactly one nonzero ADD. +Before its only `E_ij(alpha)`, dirt row i is e_i. After it the row is +`e_i+alpha m_j`, with m_j row j of the invertible prefix M. No later +operation changes that dirt row, so restoration requires `alpha m_j=0`. +Multiplication by `M^-1` gives `alpha e_j=0`, hence alpha=0, a contradiction. +Thus any used destination has K_i>=2. In particular a nonzero-demand row +with no insertion must have K_i>=2. This is the credited incoming-row +argument of #3063/#4916/#5163, not a universal per-edge count. + +**Exactly one insertion.** Suppose the word has only `P_i(beta)`. +Its final source column is `L(beta e_i)`, where L is the invertible suffix +matrix. Every demand is a multiple of beta, and `L^-1 lambda=beta e_i` +expresses beta as a combination of the demands. Consequently `(beta)=I`, +the ideal invariant from #5139, also used in #5266. In a Boolean ring a +principal ideal has a unique generator: from `(beta)=(g)` we get +`beta g=beta` and `beta g=g`, so beta=g. + +Each row other than i has no insertion and needs at least two ADDs. If row +i had no incoming ADD, its final coefficient would be beta=g, whereas +lambda_i does not generate I. Therefore row i also receives ADDs, and the +return lemma makes their number at least two. Every such word componentwise +dominates the U_i count vector. Zero insertions cannot supply nonzero demand. + +**At least two insertions.** The remaining classification is inherited from +#5259; it needs only zero sum and pairwise incomparable principal ideals, +not nonprincipality of I. We include it to avoid a dependency on that pending +proof. Let S be the set of rows receiving insertions. + +* If S contains all rows, the counts dominate D. +* If `S={i}`, then P_i>=2 and K_j,K_k>=2, so they dominate T_i. +* Suppose `S={i,j}`. Row k has K_k>=2. If P_i>=2 or P_j>=2, the + counts dominate the corresponding R vector in the table below. + Otherwise P_i=P_j=1. If either insertion row receives an ADD, it receives + at least two, giving an M vector. The remaining case has K_i=K_j=0. + +In that remaining case, parent rows i,j retain independent fixed dirt a_i,a_j +throughout. Their sole insertion coefficients must be lambda_i,lambda_j. +If only one of the two parent edges into k were used, its final source +coefficient would lie in that parent's principal ideal, contrary to +incomparability. Both edges are therefore used. Restoration of the independent +a_i and a_j requires the sum of the coefficients on each respective edge +to vanish. Each used edge needs at least two nonzero calls, so K_k>=4; +these counts dominate Q_k. This per-edge argument is valid here because +the parent dirt rows never change. + +The cases exhaust every word, including cancellations, feedback and arbitrary +interleavings. Every attainable aggregate count vector dominates one of the +twenty-two vectors below; hence every bill is at least the displayed optimum. + +## Matching constructions and irredundancy + +All words below are chronological. Let u=1_R, and let i,j,k be distinct. +Because R has characteristic two, each primitive is its own inverse. +The nonzero entries of `(P_0,P_1,P_2,K_0,K_1,K_2)` are listed here. + +| Family | Price | Nonzero counts | Number | +|---|---|---|---| +| D | `sum mu_i` | all P_i=1 | 1 | +| T_i | `2mu_i+2c_j+2c_k` | P_i=2, K_j=K_k=2 | 3 | +| R_(i,j;k) | `2mu_i+mu_j+2c_k` | P_i=2, P_j=1, K_k=2 | 6 | +| M_(i,j;k) | `mu_i+mu_j+2c_i+2c_k` | P_i=P_j=1, K_i=K_k=2 | 6 | +| Q_k | `mu_i+mu_j+4c_k` | P_i=P_j=1, K_k=4 | 3 | +| U_i | `mu_i+2 sum c_r` | P_i=1, all K_r=2 | 3 | + +The first five families use the predecessor's words: + + D: P_0(lambda_0), P_1(lambda_1), P_2(lambda_2). + + T_i: E_ji(u), P_i(lambda_j), E_ji(u), + E_ki(u), P_i(lambda_k), E_ki(u). + + R_(i,j;k): E_ki(u), P_i(lambda_k), E_ki(u), + P_i(lambda_j), P_j(lambda_j). + + M_(i,j;k): E_ij(u), E_ki(u), P_i(lambda_k), P_j(lambda_j), + E_ki(u), E_ij(u). + + Q_k: E_ki(u), E_kj(u), P_i(lambda_i), P_j(lambda_j), + E_kj(u), E_ki(u). + +An echo `E_ji(u),P_i(t),E_ji(u)` restores dirt and gives t to both rows' +source coefficients. This proves T and R using `lambda_i=lambda_j+lambda_k`. +For M, immediately before the last two gates the rows are + + A_i=a_i+a_j+lambda_k p, A_j=a_j+lambda_j p, + A_k=a_k+a_i+a_j. + +Those gates restore dirt and leave demands lambda_i,lambda_j,lambda_k. +For Q the last two gates add `lambda_i+lambda_j=lambda_k` to k's source +coefficient and restore its dirt. D is immediate. + +**U_i: one insertion, two ADDs per row.** Let C be the chronological suffix + + E_ji(lambda_j), E_ki(lambda_k), E_ij(h_i), h_i=g+lambda_i. + +It sends the source column g e_i successively to a column with entries +`g,lambda_j,lambda_k` on i,j,k, and then to lambda: its last update replaces +g by `g+h_i lambda_j=g+h_i=lambda_i`. Execute + + C^-1, P_i(g), C. + +The first word has zero source column and changes only dirt. The suffix C +undoes that dirt change and transports the inserted column to lambda. +Each destination occurs once in C and once in its inverse. All coefficients +are nonzero, giving exactly the U_i counts. For the requested instance U_0 is + + E_01(4), E_20(6), E_10(5), P_0(7), + E_10(5), E_20(6), E_01(4). + +Thus every listed vector is attained. They are pairwise incomparable, so +the lower-bound classification makes them the exact Pareto frontier. +For the stronger assertion that every linear price term is indispensable, +the following strictly positive prices uniquely expose one member per family. +Permuting row labels exposes all members; direct substitution verifies each +strict inequality against the table, and the verifier checks all permutations. + +| Unique minimum | Prices `(mu_0,mu_1,mu_2,c_0,c_1,c_2)` | Value | +|---|---|---| +| D | `(1,1,1,1,1,1)` | 3 | +| T_0 | `(1,3,3,1,1,1)` | 6 | +| R_(0,1;2) | `(1,2,5,1,2,1)` | 6 | +| M_(0,1;2) | `(3,5,10,1,3,2)` | 14 | +| Q_2 | `(3,3,5,2,2,1)` | 10 | +| U_0 | `(3,9,9,1,1,1)` | 9 | + +## Bounded verification and limitations + +The standard-library verifier checks every zero-sum incomparable ordered +triple over `F_2^n` for n=3,4,5, including proper demand ideals when n>3. +It checks all twenty-two constructors and inverses on every formal input +column, and all scalar input assignments for the requested eight-element +instance. Separate controls check the uniform-price corollary, strict exposure, +omitted dirt preparation, wrong Boolean identity, essential hypotheses and +the failure of a universal per-edge two-call bound. + +An independent packed-state bidirectional Dijkstra implementation permits +all 63 nonzero primitive gates on the full three-row affine state. It tracks +all nine dirt coefficients and three source coefficients, with the correct +heterogeneous price for each destination and operation type. There is no +length cutoff, formula-derived pruning or restriction to the proposed words. +The sum of the two queue minima is a lower bound on an uncompleted shortest +path; search stops once it reaches the best meeting length. Positive rational +prices are scaled exactly to integers. Returned paths are replayed and charged +by the separate coordinate-arithmetic ring interpreter. The seven cases +cover the six exposed families and a rational price vector; they do not +enumerate the entire affine graph or prove an all-price theorem. + +```sh +python3.12 -B scripts/research_package.py --package research/boolean-triple-fanout --check-only +python3.12 -B scripts/research_package.py --package research/boolean-triple-fanout +python3.12 -I -W error -B research/boolean-triple-fanout/verify.py +``` + +The recorded check covers 456 demands, 10,032 words, 80,256 formal +forward/inverse column checks and 180,224 literal input checks. All 22 vectors +are strictly exposed, eleven controls pass, and seven shortest-path queries +settle 314,361 states in total, counted separately per direction and query. +Their exact optima are 3, 6, 6, 14, 10, 9 and 79/30. Normal and optimized +outputs agree. Three disposable optimized-mode mutations reject an underpriced +U term, omitted one-insertion preparation and ignored heterogeneous prices. + +The verifier writes no files and needs neither Git nor network. Normal and +optimized warning-strict commands are registered; submission checks are +recorded in the PR. The general Boolean-ring and arbitrary-real-price conclusions rest on +the written proof. Independent human review and proof-kernel acceptance are +unclaimed. Independently priced directed edges, extra helpers, restricted +coefficients and non-Boolean rings are outside this theorem. Physical source +access, coefficient production, routing, precision, stock and supplier admission +remain separate obligations; the selected frontier is unchanged. + +## Sources and coordination + +The scientific base is canonical main +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority revision 7. +TASK.json retains the original `bit-helper-contract` card and records the +explicit donor assignment as a changed algebraic side-result scope. The +SOURCES.json Git pins refer to this main ancestor. Exact bibliographic pins +for pending #5259 document adapted arguments, words and verifier infrastructure; +its files are not runtime inputs, and no unmerged Git object is needed by replay. +All proof steps and executable code needed for this result are included here. + +The preceding survey paginated 347 open PRs and 4,548 Discussion records +on 2026-10-23, followed by entry-time all-state fanout PR searches and live +board/#1166/#5030 checks at 16:29 UTC. #5266 settles insertion count only; +#5269 concerns matrix-ring feasibility. Neither supplies this tariff. No +same-tariff resolution or overlapping active claim appeared in the inspected +records. Sparse local notes, arbitrary historical diffs and unpublished work +remain coverage limits. The +[canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/5030#discussioncomment-19149863) +records the scoped claim and final artifact. Submission freshness is in the PR. +The submission refresh also read Ali Romman's new +[Discussion #5300](https://github.com/CrocSwap/integer-mult-bounds/discussions/5300): +its extension to all finite associative rings explicitly concerns insertion +count, with total tariffs left open, so it does not resolve this contribution. + +## Open next questions + +1. Determine the exact tariff for the same Boolean triple with independent + positive prices on all six directed ADD edges. Start with cheap directed + cycles and the seven-gate U witnesses. Aggregate destination counts discard + parent identities, and the return lemma cannot charge each edge twice. +2. Determine the tariff for the incomparable Boolean triple `(1,2,4)` over + `F_2^3`, which does not sum to zero. Single-insertion feasibility is already + covered by #5266. Begin by finding a least-ADD conjugating suffix from a + unit source column, then classify multi-insertion support. The zero-sum + constructions and Boolean atom pattern proved here do not supply that bound. + +The structured questions and blockers are in [TASK.json](TASK.json). These +are suggested obligations, not claims of reservation or exhaustive novelty. + +## Credit + +Prepared by lee-phys with substantial OpenAI Codex assistance in source +inspection, derivation, implementation, verification and writing; no subagents +or independent reviewers were used. Apache-2.0. The new result adds the sharp +single-insertion branch and proves its Boolean-ring scope. The nineteen +multi-insertion vectors, their words and portions of the verifier infrastructure +are adapted from lee-phys #5259 at the exact head cited above. Credit Ali Romman +#5266 for the many-row insertion-count theorem; lee-phys #5139/#5163 for +ideal invariance and the local-ring boundary; Nick Petalas #5208/#4916 for +equal-demand tariffs and the ring-valued contract; Krzysztof Wojt #5045 for +source-support classification and restoring words; Ross Richardson #3063/#3121 +for tariffs and incoming-row restoration; and Cinna Davis, Anthony, Oscar +Fennell, Tekalign and the retained earlier fanout lineage. diff --git a/research/boolean-triple-fanout/SOURCES.json b/research/boolean-triple-fanout/SOURCES.json new file mode 100644 index 0000000000..0c3f450e47 --- /dev/null +++ b/research/boolean-triple-fanout/SOURCES.json @@ -0,0 +1,56 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/finite-commutative-fanout/README.md", + "usage": "provenance", + "git_blob": "46e0adf1ac10ba982a30d98e2bdcf13e1f744a4e", + "sha256": "0d8895504797f796534a64303c5780b2897c0b8e6b1b9dec3dca84ac14ffc197" + }, + { + "path": "research/local-ring-row-fanout/README.md", + "usage": "provenance", + "git_blob": "a65ecdb615300c6b4357eadadb52b46cfbc363ba", + "sha256": "4f167d526d889089717b9ba273bc7d048efe4ec1e02cdd91456543e7fc9703fb" + } + ], + "bibliographic_sources": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/d2a7d88f011ca9c520333da8d4e03f1f22d23e91/research/square-zero-triple-fanout/README.md", + "commit": "d2a7d88f011ca9c520333da8d4e03f1f22d23e91", + "sha256": "4e46d3aa0265b79f460c9475f66c3a755c3ed5c1d66a2c6b56cceb8ab0bb7c22", + "role": "Attribution for adapted arguments, constructions and verifier infrastructure. Not a Git provenance pin or runtime input; adapted material is self-contained in this package." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/d2a7d88f011ca9c520333da8d4e03f1f22d23e91/research/square-zero-triple-fanout/verify.py", + "commit": "d2a7d88f011ca9c520333da8d4e03f1f22d23e91", + "sha256": "f671e3b8bf702e47111f143fd668ef3f188af8b3d3068ae49859fd19745721c1", + "role": "Attribution for adapted arguments, constructions and verifier infrastructure. Not a Git provenance pin or runtime input; adapted material is self-contained in this package." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5266", + "author": "Ali Romman", + "observed_updated_at": "2026-10-23T14:56:13Z", + "role": "Credits the prior many-row source-insertion count theorem; no source or runtime dependency." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5300", + "author": "Ali Romman", + "observed_updated_at": "2026-10-23T16:35:48Z", + "role": "Submission-time successor extends insertion count to finite associative rings; explicitly does not determine total tariffs. Attribution only, no runtime dependency." + } + ] +} diff --git a/research/boolean-triple-fanout/TASK.json b/research/boolean-triple-fanout/TASK.json new file mode 100644 index 0000000000..2124cbd2d8 --- /dev/null +++ b/research/boolean-triple-fanout/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "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", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the exact arbitrary-positive destination-row tariff and complete 22-vector Pareto frontier for demand (110,101,011) over F2^3; extend the proof to zero-sum triples with pairwise incomparable principal ideals over any commutative unital Boolean ring.", + "scope_change_reason": "The donor explicitly assigned the principal-ideal Boolean triple left open by #5259. This is an algebraic side result, not an H2/K replacement or a physical bit-supplier expansion.", + "bottleneck_link": "Supplies a complete abstract dirty-input cost and all-word lower bound. Physical source access, coefficient production, routing, precision, stock and supplier interfaces still need separate accounting; no new kappa.", + "budget_minutes": 60, + "stop_rule": "Finish a self-contained lower bound with a construction for every necessary price term, or record the precise unresolved branch. Bound corroboration to three small Boolean rings and seven independent shortest-path price cases.", + "outcome": "completed", + "evidence": "README.md proves the all-word 22-term optimum, exact count-vector frontier, strict exposure and Boolean-ring extension. verify.py checks 456 demands, 10032 words, 80256 formal forward/inverse column checks, 180224 literal input checks, all 22 strict price witnesses, 11 controls and seven independent full-state shortest paths settling 314361 states. Finite evidence corroborates the written proof; independent human review and proof-kernel acceptance are unclaimed.", + "author": "lee-phys, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in source inspection, derivation, proof, implementation, exact experiments, validation and writing. No subagents or independent reviewers were used.", + "open_questions": [ + { + "question": "What is the exact tariff for (110,101,011) over F2^3 with independent positive prices on the six directed ADD edges?", + "why_it_matters": "The destination-only frontier loses parent identities and does not price arbitrary routing.", + "first_step": "Probe cheap directed cycles with full dirt tracking and compare them with all row-labeled seven-gate one-insertion words.", + "blocked_by": "The incoming-row return lemma is not a per-edge bound; aggregate destination counts cannot supply the required edge-sensitive lower bound." + }, + { + "question": "What is the exact destination-row tariff for demand (1,2,4) over F2^3?", + "why_it_matters": "This incomparable principal-ideal triple has no zero-sum relation; source-insertion feasibility is known from #5266 but total tariff is not established here.", + "first_step": "Find the least-ADD source-column conjugations from a unit insertion and classify multi-insertion support with all original dirt columns retained.", + "blocked_by": "The present zero-sum words and three-atom demand pattern do not apply. A new matching count classification is needed." + } + ] +} diff --git a/research/boolean-triple-fanout/VERIFY.json b/research/boolean-triple-fanout/VERIFY.json new file mode 100644 index 0000000000..c0acf38786 --- /dev/null +++ b/research/boolean-triple-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": 360, + "checks": "Normal exact Boolean-ring constructors and inverses, all 22 exposed vectors, literal eight-element input checks, 11 controls and seven independent packed-state shortest paths." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 360, + "checks": "Optimized exact Boolean-ring constructors and inverses, all 22 exposed vectors, literal eight-element input checks, 11 controls and seven independent packed-state shortest paths." + } + ] +} diff --git a/research/boolean-triple-fanout/verify.py b/research/boolean-triple-fanout/verify.py new file mode 100644 index 0000000000..eeed466cc5 --- /dev/null +++ b/research/boolean-triple-fanout/verify.py @@ -0,0 +1,373 @@ +#!/usr/bin/env python3 +"""Exact bounded checks for the Boolean triple tariff; Apache-2.0. + +lee-phys with substantial OpenAI Codex assistance. Adapted word, interpreter +and Dijkstra infrastructure from #5259, head d2a7d88f011ca9c520333da8d4e03f1f22d23e91. +Credit #5045/#5139/#5163/#5208 and the earlier fanout lineage in README.md. +""" +from dataclasses import dataclass +from fractions import Fraction +from heapq import heappop, heappush +from itertools import permutations, product +from math import lcm +import json + + +def require(test, message): + if not test: + raise RuntimeError(message) + + +@dataclass(frozen=True) +class Ring: + name: str + n: int + one: int + add: tuple + mul: tuple + + def neg(self, x): + return next(y for y in range(self.n) if self.add[x][y] == 0) + + def principal(self, x): + return frozenset(self.mul[a][x] for a in range(self.n)) + + def ideal(self, xs): + out = frozenset([0]) + for x in xs: + out = frozenset(self.add[a][b] for a in out for b in self.principal(x)) + return out + + +def ring_from_functions(name, n, one, add, mul): + return Ring(name, n, one, tuple(tuple(add(x, y) for y in range(n)) for x in range(n)), + tuple(tuple(mul(x, y) for y in range(n)) for x in range(n))) + + +def check_ring(r): + es = range(r.n) + for a, b in product(es, repeat=2): + require(r.add[a][b] in es and r.mul[a][b] in es, 'ring closure') + require(r.add[a][b] == r.add[b][a] and r.mul[a][b] == r.mul[b][a], 'commutative ring') + for a in es: + require(r.add[a][0] == a and r.mul[a][r.one] == a and r.mul[a][0] == 0, 'ring identities') + require(r.add[a][r.neg(a)] == 0, 'additive inverse') + for a, b, c in product(es, repeat=3): + require(r.add[r.add[a][b]][c] == r.add[a][r.add[b][c]], 'addition associativity') + require(r.mul[r.mul[a][b]][c] == r.mul[a][r.mul[b][c]], 'multiplication associativity') + require(r.mul[a][r.add[b][c]] == r.add[r.mul[a][b]][r.mul[a][c]], 'distributivity') + + +def patterns(): + out = [('D', 0, 1, 2, (1, 1, 1, 0, 0, 0))] + for i in range(3): + j, k = [r for r in range(3) if r != i] + v = [0]*6 + v[i], v[3+j], v[3+k] = 2, 2, 2 + out.append(('T', i, j, k, tuple(v))) + for mode in ('R', 'M'): + for i, j, k in permutations(range(3)): + v = [0]*6 + v[i], v[j], v[3+k] = 1, 1, 2 + if mode == 'R': + v[i] = 2 + else: + v[3+i] = 2 + out.append((mode, i, j, k, tuple(v))) + for k in range(3): + i, j = [r for r in range(3) if r != k] + v = [0]*6 + v[i], v[j], v[3+k] = 1, 1, 4 + out.append(('Q', i, j, k, tuple(v))) + for i in range(3): + j, k = [r for r in range(3) if r != i] + v = [0, 0, 0, 2, 2, 2] + v[i] = 1 + out.append(('U', i, j, k, tuple(v))) + return out + + +def construct(r, d, pattern): + mode, i, j, k, _ = pattern + u, v = r.one, r.neg(r.one) + if mode == 'D': + return [(t, 3, d[t]) for t in range(3)] + if mode == 'T': + return [(j, i, u), (i, 3, r.neg(d[j])), (j, i, v), + (k, i, u), (i, 3, r.neg(d[k])), (k, i, v)] + if mode == 'R': + return [(k, i, u), (i, 3, r.neg(d[k])), (k, i, v), + (i, 3, r.neg(d[j])), (j, 3, d[j])] + if mode == 'M': + return [(i, j, u), (k, i, u), (i, 3, r.neg(d[k])), (j, 3, d[j]), + (k, i, v), (i, j, v)] + if mode == 'Q': + return [(k, i, u), (k, j, u), (i, 3, d[i]), (j, 3, d[j]), (k, j, v), (k, i, v)] + if mode == 'U': + g = r.add[r.add[d[0]][d[1]]][r.mul[d[0]][d[1]]] + suffix = [(j, i, d[j]), (k, i, d[k]), (i, j, r.add[g][d[i]])] + return inverse(r, suffix)+[(i, 3, g)]+suffix + raise ValueError('unknown word family') + + +def inverse(r, word): + return [(i, j, r.neg(a)) for i, j, a in reversed(word)] + + +def execute(r, word, entry): + out = list(entry) + for i, j, a in word: + out[i] = r.add[out[i]][r.mul[a][out[j]]] + return tuple(out) + + +def target(r, d, entry): + return tuple(r.add[entry[i]][r.mul[d[i]][entry[3]]] for i in range(3))+(entry[3],) + + +def endpoint(r, d, word): + for k in range(4): + entry = tuple(r.one if j == k else 0 for j in range(4)) + want = target(r, d, entry) + if execute(r, word, entry) != want or execute(r, inverse(r, word), want) != entry: + return False + return True + + +def counts(word): + return tuple(sum(i == k and j == 3 for i, j, _ in word) for k in range(3))+tuple( + sum(i == k and j != 3 for i, j, _ in word) for k in range(3)) + + +def bill(word, prices): + return sum(prices[i if j == 3 else 3+i] for i, j, _ in word) + + +def neighbors(state, weights, tables): + rows = [(state >> (12*i)) & 4095 for i in range(3)] + for i in range(3): + for a in range(1, 8): + yield state ^ (a << (12*i+9)), weights[i], (i, 3, a) + for j in range(3): + if j != i: + for a in range(1, 8): + yield state ^ (tables[a][rows[j]] << (12*i)), weights[3+i], (i, j, a) + + +def oracle(demand, prices, tables): + scale = lcm(*(Fraction(x).denominator for x in prices)) + weights = tuple(int(Fraction(x)*scale) for x in prices) + require(min(weights) > 0, 'positive oracle weights') + start = 7 | (56 << 12) | (448 << 24) + goal = start | sum(x << (12*i+9) for i, x in enumerate(demand)) + ds = [{start: 0}, {goal: 0}] + qs = [[(0, start)], [(0, goal)]] + ps = [{start: None}, {goal: None}] + best, meet = None, None + settled = [0, 0] + while qs[0] and qs[1]: + for s in (0, 1): + while qs[s] and qs[s][0][0] != ds[s][qs[s][0][1]]: + heappop(qs[s]) + if not qs[0] or not qs[1]: + break + if best is not None and qs[0][0][0]+qs[1][0][0] >= best: + break + s = int(qs[1][0][0] < qs[0][0][0]) + du, u = heappop(qs[s]) + settled[s] += 1 + for v, cost, gate in neighbors(u, weights, tables): + dv = du+cost + if v not in ds[s] or dv < ds[s][v]: + ds[s][v] = dv + ps[s][v] = (u, gate) + heappush(qs[s], (dv, v)) + if v in ds[1-s]: + candidate = dv+ds[1-s][v] + if best is None or candidate < best: + best, meet = candidate, v + require(meet is not None, 'oracle endpoints disconnected') + forward, back = [], [] + u = meet + while ps[0][u] is not None: + u, gate = ps[0][u] + forward.append(gate) + u = meet + while ps[1][u] is not None: + u, gate = ps[1][u] + back.append(gate) # Every primitive inverse equals itself in characteristic two. + return Fraction(best, scale), list(reversed(forward))+back, settled + + +def boolean_ring(n): + # Coordinate arithmetic supplies the primary tables, independently of the + # packed oracle's bitwise-AND implementation. + return ring_from_functions(f'F2^{n}', 2**n, 2**n-1, + lambda a, b: sum((((a//2**k) % 2+(b//2**k) % 2) % 2)*2**k for k in range(n)), + lambda a, b: sum(((a//2**k) % 2)*((b//2**k) % 2)*2**k for k in range(n))) + + +def validate_demand(r, d): + if any(r.mul[x][x] != x for x in range(r.n)): + raise ValueError('a Boolean ring is required') + if len(d) != 3 or any(type(x) is not int or not 0 <= x < r.n for x in d): + raise ValueError('three ring elements required') + if r.add[r.add[d[0]][d[1]]][d[2]] != 0: + raise ValueError('the demand must sum to zero') + if any(d[i] in r.principal(d[j]) for i in range(3) for j in range(3) if i != j): + raise ValueError('pairwise incomparable principal ideals required') + + +def formula(mu, c): + if len(mu) != 3 or len(c) != 3 or min((*mu, *c)) <= 0: + raise ValueError('six strictly positive prices required') + out = [sum(mu), min(mu)+2*sum(c)] + for k in range(3): + i, j = [r for r in range(3) if r != k] + out.append(2*mu[k]+2*c[i]+2*c[j]) + out.append(mu[i]+mu[j]+2*c[k]+min(mu[i], mu[j], 2*c[i], 2*c[j], 2*c[k])) + return min(out) + + +def packed_tables(): + # Four 3-bit coefficients in each 12-bit row; multiplication is AND. + return [None]+[tuple(x & (a | a << 3 | a << 6 | a << 9) for x in range(4096)) + for a in range(1, 8)] + + +def main(): + pats = patterns() + vectors = [p[-1] for p in pats] + require(len(vectors) == len(set(vectors)) == 22, 'twenty-two distinct vectors') + require(all(not all(a <= b for a, b in zip(v, w)) for v in vectors for w in vectors if v != w), + 'Pareto vectors incomparable') + total = dict(demands=0, words=0, formal_forward_inverse=0, literal_forward_inverse=0, + exposed_vectors=0, oracle_queries=0, oracle_settled=0, controls=0) + fixtures = [] + for n in (3, 4, 5): + r = boolean_ring(n) + check_ring(r) + accepted = proper = 0 + for a, b in product(range(r.n), repeat=2): + d = (a, b, r.add[a][b]) + if any(d[i] in r.principal(d[j]) for i in range(3) for j in range(3) if i != j): + continue + validate_demand(r, d) + g = r.add[r.add[a][b]][r.mul[a][b]] + require(r.ideal(d) == r.principal(g), 'principal demand ideal') + require(all(r.principal(x) != r.principal(g) for x in d), 'no demand generates I') + atoms = [r.mul[d[i]][d[j]] for i, j in ((0,1),(0,2),(1,2))] + require(all(atoms) and all(r.mul[x][y] == 0 for x,y in permutations(atoms,2)), + 'three disjoint nonzero atoms') + accepted += 1 + proper += int(g != r.one) + for pattern in pats: + word = construct(r, d, pattern) + require(all(a != 0 and 0 <= i < 3 and 0 <= j < 4 and i != j for i,j,a in word), + 'nonzero legal gates') + require(endpoint(r, d, word), 'constructed dirt endpoint/inverse') + require(counts(word) == pattern[-1], 'claimed gate counts') + total['words'] += 1 + total['formal_forward_inverse'] += 8 + require(accepted == 4**n-3*3**n+3*2**n-1, 'all three support atoms nonempty') + total['demands'] += accepted + fixtures.append({'ring': r.name, 'demands': accepted, 'proper_ideal_demands': proper}) + + r, d = boolean_ring(3), (3,5,6) + words = [construct(r, d, p) for p in pats] + for word in words: + rev = inverse(r, word) + for entry in product(range(8), repeat=4): + want = target(r, d, entry) + require(execute(r, word, entry) == want and execute(r, rev, want) == entry, + 'literal eight-element endpoint/inverse') + total['literal_forward_inverse'] += 2 + + representatives = [(1,1,1,1,1,1), (1,3,3,1,1,1), (1,2,5,1,2,1), + (3,5,10,1,3,2), (3,3,5,2,2,1), (3,9,9,1,1,1)] + exposed = set() + for prices in representatives: + for perm in permutations(range(3)): + p = tuple(prices[i] for i in perm)+tuple(prices[3+i] for i in perm) + costs = [bill(word, p) for word in words] + minimum = min(costs) + require(costs.count(minimum) == 1, 'strict positive-price exposure') + require(minimum == formula(p[:3], p[3:]), 'compressed twenty-two-term envelope') + exposed.add(costs.index(minimum)) + require(len(exposed) == 22, 'every vector exposed by positive prices') + total['exposed_vectors'] = len(exposed) + for mu, c in product(range(1,13), repeat=2): + require(formula((mu,)*3, (c,)*3) == min(3*mu, mu+6*c), 'uniform-price corollary') + + # The old nineteen-term formula is strictly too expensive for this demand. + p = (10,100,100,1,1,1) + require(min(bill(w,p) for w in words[:19]) == 24 and formula(p[:3],p[3:]) == 16, + 'one-insertion branch changes the optimum') + total['controls'] += 1 + for bad, fragment in [((3,5,3),'sum to zero'), ((1,1,0),'incomparable')]: + try: + validate_demand(r, bad) + except ValueError as error: + require(fragment in str(error), 'correct hypothesis rejection') + total['controls'] += 1 + else: + raise RuntimeError('accepted out-of-scope demand') + require(not endpoint(r, (3,5,3), construct(r,(3,5,3),pats[1])), 'zero sum is substantive') + total['controls'] += 1 + # The first three preparations of U_0 do not act on a zero source column. + corrupted = words[19][3:] + require(execute(r, corrupted, (0,0,0,7)) == (*d,7), 'dirty-only corruption premise') + require(not endpoint(r, d, corrupted), 'reject omitted one-insertion dirt preparation') + total['controls'] += 1 + wrong = [g if g[1] != 3 else (g[0],g[1],1) for g in words[19]] + require(not endpoint(r, d, wrong), 'Boolean identity is 7, not bitmask 1') + total['controls'] += 1 + relator = [(0,1,7),(1,2,7),(0,1,7),(1,2,7),(0,2,7)] + require(endpoint(r, (0,0,0), relator), 'identity with one call on edge 02') + total['controls'] += 1 + # Outside the incomparable-ideal hypothesis, a two-ADD echo costs only 5. + comparable = (1,1,0) + echo = [(1,0,7),(0,3,1),(1,0,7)] + p = (1,9,9,1,2,1) + require(endpoint(r,comparable,echo) and bill(echo,p) == 5 < formula(p[:3],p[3:]), + 'pairwise incomparability is substantive') + total['controls'] += 1 + z4 = ring_from_functions('Z/4',4,1,lambda a,b:(a+b)%4,lambda a,b:a*b%4) + try: + validate_demand(z4,(1,1,2)) + except ValueError as error: + require('Boolean' in str(error), 'non-Boolean rejection') + total['controls'] += 1 + else: + raise RuntimeError('accepted non-Boolean ring') + for bad_prices in [(0,1,1,1,1,1),(1,1,1,-1,1,1)]: + try: + formula(bad_prices[:3],bad_prices[3:]) + except ValueError: + total['controls'] += 1 + else: + raise RuntimeError('accepted nonpositive prices') + + tables = packed_tables() + for a in range(1,8): + for x in range(4096): + require(tables[a][x] == sum(r.mul[a][(x >> (3*k)) & 7] << (3*k) for k in range(4)), + 'oracle multiplication agrees with coordinate arithmetic') + cases = list(zip(('D','T','R','M','Q','U'), representatives)) + cases += [('rational', (Fraction(1,2),Fraction(4,3),Fraction(7,3), + Fraction(2,3),Fraction(3,4),Fraction(1,5)))] + results = [] + for name, prices in cases: + value, path, settled = oracle(d, prices, tables) + require(value == formula(prices[:3], prices[3:]), f'oracle mismatch: {name}') + require(endpoint(r,d,path) and bill(path,prices) == value, 'oracle path replay and price') + total['oracle_queries'] += 1 + total['oracle_settled'] += sum(settled) + results.append({'case': name, 'optimum': str(value), 'settled': settled}) + print('CHECK_ORACLE', name, str(value), flush=True) + print(json.dumps({'fixtures': fixtures, 'counts': total, 'oracle': results}, sort_keys=True)) + print('PASS_BOOLEAN_TRIPLE_FANOUT no_new_kappa') + + +if __name__ == '__main__': + main()