diff --git a/research/orthogonal-boolean-fanout/README.md b/research/orthogonal-boolean-fanout/README.md new file mode 100644 index 0000000000..fa02e1e585 --- /dev/null +++ b/research/orthogonal-boolean-fanout/README.md @@ -0,0 +1,347 @@ +# Exact tariffs for three orthogonal Boolean demands + +**Scoped written proof with exact finite corroboration; no new kappa.** +For three arbitrary dirty rows over `F_2^3`, demand +`((1,0,0),(0,1,0),(0,0,1))` has an exact **twenty-five-term** optimum at +all positive source-insertion and destination-row ADD prices. Every listed +price term is attained and indispensable. The proof applies to any three +nonzero pairwise orthogonal elements of any commutative unital Boolean ring. + +This resolves Open next question 2 of lee-phys's +[PR #5304](https://github.com/CrocSwap/integer-mult-bounds/pull/5304), +head `c8bf34c359b3a12f112078f0072b4ecc7a942109`. That theorem concerns +zero-sum demands `(3,5,6)`, not the present `(1,2,4)` (bitmask notation). +Ali Romman's [#5310](https://github.com/CrocSwap/integer-mult-bounds/pull/5310) +already determines the minimum source-insertion count; this contribution +prices the complete restoring word. The new steps are the sharp weighted +one-insertion bound, the exclusion of the two-fixed-parent branch, and +matching non-zero-sum constructions. The proof is self-contained. + +## Contract and exact formula + +Let R be a commutative unital Boolean ring, `1 != 0`, so `x^2=x` for all x. +Expanding `(x+1)^2=x+1` gives `2x=0`. There are exactly three independent +arbitrary dirty rows `a_i in R^w`, w >= 1, and a disjoint preserved source +`p in R^w`. For every input, a fixed finite word must produce + + A_i = a_i + lambda_i p, i=0,1,2. + +The only gates 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 ring coefficients and ordered row pairs are allowed. Prices are finite, +stationary, coefficient-independent complete abstract prices. There are no +extra rows, observations, adaptive choices, clearing or free basis changes. +All original dirt columns must return; separate inverse execution is charged +separately. Zero-coefficient gates can be deleted since prices are positive. + +**Theorem.** Assume every lambda_i is nonzero and +`lambda_i lambda_j=0` for distinct i,j. Set `g=lambda_0+lambda_1+lambda_2`. +For distinct i,j,k and arbitrary h in `{0,1,2}`, 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), + U_(i,h) = mu_i + 2(c_0+c_1+c_2) + 2c_h. + +Then the exact optimum over every allowed finite word is + + OPT = min(D, T_0,T_1,T_2, B_0,B_1,B_2, + min_i(mu_i) + 2 sum_i(c_i) + 2 min_i(c_i)). + +Expanding the minima gives 1 D term, 3 T terms, 12 B terms and 9 U terms: +**25 indispensable linear price terms**. Minimizers in the last term may +choose the insertion row and the cheapest ADD row independently. +The formula and an attaining word require a constant number of comparisons +once the ring hypotheses and prices are supplied; testing those hypotheses +or implementing the abstract primitives is not included. + +For the requested ring, encode `(x_0,x_1,x_2)` as `x_0+2x_1+4x_2`. +Addition is XOR, multiplication is AND, identity is 7, and demand is `(1,2,4)`. +At `mu=(10,100,100), c=(1,1,1)`, the exact cost is **18**; the zero-sum +predecessor's value 16 is inapplicable. With common prices mu and c, + + OPT = min(3mu, mu+8c). + +Indeed the other potentially competitive term is `2mu+4c`, the arithmetic +mean of these two quantities. The transition is `mu=4c`; two-insertion +words also tie there. A one-insertion word needs at least eight ADDs and +can attain that number. For root 0 and the extra two ADDs charged to row 0: + + E_02(4), E_01(2), E_20(4), E_10(2), P_0(7), + E_10(2), E_20(4), E_01(2), E_02(4). + +## Algebra and the incoming-row return lemma + +Orthogonality gives `g lambda_i=lambda_i` and +`(lambda_0,lambda_1,lambda_2)=(g)`. Also `g!=lambda_i` for each i: multiply +an alleged equality by any other nonzero lambda_j. No lambda_k belongs +to `(lambda_i,lambda_j)` when i,j,k are distinct, since multiplying such +an expression by lambda_k would imply `lambda_k^2=lambda_k=0`. +In particular each pair of principal demand ideals is incomparable. +Finiteness of R and a decomposition into fields are not assumed. + +Let P_i count nonzero source insertions into i, and K_i count all incoming +nonzero ADDs. Prefix dirt matrices are invertible: each elementary row ADD +has an inverse (the same gate here), and P gates do not change dirt. Testing +each original input column separately forces the final dirt matrix to be I. + +**Return lemma.** A row cannot receive exactly one nonzero ADD. Before +its only `E_ij(alpha)`, its dirt row is e_i. If the prefix dirt matrix is M, +after that gate its dirt row is `e_i+alpha m_j`. No later gate changes this +dirt row. Restoration would give `alpha m_j=0`; multiplying by `M^-1` +gives `alpha e_j=0`, hence alpha=0, a contradiction. Thus every used ADD +destination has K_i>=2. A nonzero-demand row with no insertion needs ADDs +and consequently K_i>=2. + +This is the credited incoming-row argument of #3063/#4916/#5163. It does +not say every used directed edge occurs twice; a control retains the +five-ADD identity from #5163 that disproves that stronger statement. + +## The new one-insertion lower bound + +Suppose exactly one insertion `P_i(beta)` occurs. Write M for the ADD-only +prefix dirt matrix and L for the ADD-only suffix dirt matrix. Restoration +requires `LM=I`, and the final source column is `L(beta e_i)=lambda`. +Thus every lambda_r is a multiple of beta, and `L^-1 lambda=beta e_i` +expresses beta as a combination of the demands. Hence `(beta)=(g)`. +A principal ideal in a Boolean ring has a unique generator: writing +`beta=xg` and `g=y beta` yields `beta g=beta` and `beta g=g`, respectively. +Therefore **beta=g**. This uses the ideal invariant from #5139/#5310. + +**Column lemma.** Any ADD-only word taking `g e_i` to lambda costs at least + + c_0+c_1+c_2 + min(c_0,c_1,c_2). + +Every row must be an ADD destination: the two other rows start at zero and +end nonzero, and row i starts at g and ends at `lambda_i!=g`. Three gates +would therefore update each row exactly once. At the sole update of i, +its parent j has source coefficient either zero (before j's sole update) +or lambda_j (after it). The zero case cannot change g. In the other case, +`g+alpha lambda_j=lambda_i` is impossible: multiplying by the remaining +lambda_k gives `lambda_k=0`. Thus at least four gates are necessary, at +least one into each row. Their positive-price bill is at least the stated +sum plus the cheapest possible fourth gate. The argument covers arbitrarily +long words, since any word has at least those counts. + +Apply this lemma both to the suffix and to the inverse prefix. Indeed, +`M^-1=L`, so each maps `g e_i` to lambda. Inversion preserves the number of +gates charged to each destination. The original prefix and suffix therefore +cost at least twice the column bound. Including the insertion gives + + bill >= mu_i + 2 sum_r(c_r) + 2 min_r(c_r). + +This proves the one-insertion part for arbitrary interleavings: with one P +there is exactly an ADD prefix and an ADD suffix, and neither is free. +It also explains why charging only one extra ADD beyond the old six-ADD +return bound would be insufficient. No insertions cannot supply nonzero demand. + +## The multi-insertion lower bound + +Now suppose there are at least two insertions. Let S be their row support. +This classification adapts #5259/#5304; the final case changes because the +present third demand is outside the ideal of the other two. + +* If S contains all rows, the counts dominate D. +* If `S={i}`, then P_i>=2 and K_j,K_k>=2, giving T_i. +* If `S={i,j}`, then K_k>=2. A repeated insertion in i or j gives respectively + `2mu_i+mu_j+2c_k` or `mu_i+2mu_j+2c_k`. +* Otherwise P_i=P_j=1. If i or j receives any ADD, the return lemma gives + respectively `mu_i+mu_j+2c_k+2c_i` or `mu_i+mu_j+2c_k+2c_j`. +* The only remaining possibility has K_i=K_j=0. The insertion coefficients + must then be lambda_i and lambda_j, since these rows never receive ADDs. + Row k can acquire only source coefficients in `(lambda_i,lambda_j)`; + its target lambda_k lies outside that ideal. This case is impossible. + +Taking the minimum of the four feasible terms for S={i,j} gives B_k. +The proof covers feedback, cancelling insertions, arbitrary coefficients +and arbitrary word lengths. Together with the one-insertion bound it proves +the displayed lower bound for every word and every strictly positive real price. + +## Matching constructions + +All words below are chronological; i,j,k are distinct. An echo + + E_ji(a), P_i(b), E_ji(a) + +returns all dirt, adds b to i's source coefficient and adds ab to j's. +This holds even when i already has a source coefficient: its pre-existing +value cancels between the two E gates. In characteristic two each gate is +its own inverse; reverse the gate order to invert a word. + +| Family | Nonzero counts in `(P_0,P_1,P_2,K_0,K_1,K_2)` | Number | +|---|---|---| +| D | all P_i=1 | 1 | +| T_i | P_i=2, K_j=K_k=2 | 3 | +| R_(i,j;k) | P_i=2, P_j=1, K_k=2 | 6 | +| M_(i,j;k) | P_i=P_j=1, K_i=K_k=2 | 6 | +| U_(i,h) | P_i=1, all K_r=2, with two additional ADDs into h | 9 | + +**D:** insert `P_i(lambda_i)` in each row. + +**T_i:** use + + E_ji(lambda_j), P_i(g), E_ji(lambda_j), + E_ki(lambda_k), P_i(g+lambda_i), E_ki(lambda_k). + +Row i receives `g+(g+lambda_i)=lambda_i`. The echoes give lambda_j to j +and `lambda_k(g+lambda_i)=lambda_k` to k. + +**R_(i,j;k):** use + + E_ki(lambda_k), P_i(lambda_i+lambda_k), E_ki(lambda_k), + P_i(lambda_k), P_j(lambda_j). + +The echo gives lambda_k to k; the two i insertions sum to lambda_i. +The j insertion is direct. These are the first two expanded B terms. + +**M_(i,j;k):** let the two-gate suffix C be + + E_ki(lambda_k), E_ik(lambda_k). + +It sends `(lambda_i+lambda_k)e_i` to `lambda_i e_i+lambda_k e_k`. +Execute `C^-1, P_i(lambda_i+lambda_k), C`, followed by `P_j(lambda_j)`. +The conjugation restores dirt and has two ADDs each into i and k. These +are the other two expanded B terms (choose which insertion row receives ADDs). + +**U_(i,h):** build a four-gate suffix C taking `g e_i` to lambda, with +one gate into each row and one extra into h. If h=i, use + + E_ji(lambda_j), E_ki(lambda_k), E_ij(lambda_j), E_ik(lambda_k). + +The first two gates fill j,k; the last two remove lambda_j and lambda_k +from g at i. If h is another row, relabel it j, let k be the third row, +and write `q=lambda_j+lambda_k`. Use + + E_ji(q), E_ki(lambda_k), E_ij(q), E_jk(lambda_k). + +Its source column, in i,j,k order, evolves as + + (g,0,0) -> (g,q,0) -> (g,q,lambda_k) + -> (lambda_i,q,lambda_k) -> (lambda_i,lambda_j,lambda_k). + +Here `q^2=q`, `g+q=lambda_i`, and `lambda_k^2=lambda_k`. Execute +`C^-1, P_i(g), C`. Dirt returns and the inserted column becomes lambda. +The extra two ADDs can therefore be placed in **any** row h, independently +of the insertion row i. This attains every U term and the weighted column bound. + +All coefficients in these words are nonzero: sums of distinct nonzero +orthogonal demands cannot vanish. Thus the displayed counts are exact. +Every lower-bound price term is attained, completing the theorem. + +## Every price term is necessary + +The following strictly positive price vectors uniquely minimize the indicated +term among all 25. Permuting row labels supplies the remaining terms. Direct +substitution into the table verifies the strict inequalities; the verifier +checks all permutations with exact arithmetic. + +| Unique minimum | `(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 | +| U_(0,0) | `(5,9,9,1,2,2)` | 17 | +| U_(0,1) | `(7,12,12,2,1,2)` | 19 | + +This is an exact **price envelope**, not a claim that these are every +componentwise minimal attainable count vector. The one-insertion lower +bound is weighted; it does not prove componentwise domination by one U +vector when different rows carry the excess prefix and suffix gates. +The possible additional, unexposed Pareto vectors are a separate question. + +## Bounded verification and limitations + +The self-contained standard-library verifier checks all ordered nonzero +orthogonal demand triples over `F_2^n`, n=3,4,5, including proper demand +ideals. It checks all 25 words and inverses on all four formal input columns, +then all scalar inputs for the requested eight-element instance. It also +checks every strict price exposure and the uniform-price corollary. + +An independent source-column Dijkstra search permits every nonzero coefficient +and every directed ADD, for each root and each destination-price vector in +`{1,2,3}^3`. Its 81 exact answers corroborate the column lemma and the +sharp weighted bound. This projection alone does not check dirt restoration. + +A separate packed-state bidirectional Dijkstra search tracks all nine dirt +and three source coefficients and allows all 63 nonzero gates. It has no +word-length cutoff, formula-dependent pruning or restriction to displayed +constructions. The sum of the frontier minima certifies the best meeting +cost. Rational prices are scaled exactly to integers, and each returned path +is replayed by the coordinate-arithmetic interpreter. Its five price queries +cover D/T/R/M and a rational fixture; the U branches are corroborated by the +column searches and full endpoint replay, not by those five full-state queries. +The all-price theorem rests on the written proof, not on finite sampling. + +```sh +python3.12 -B scripts/research_package.py --package research/orthogonal-boolean-fanout --check-only +python3.12 -B scripts/research_package.py --package research/orthogonal-boolean-fanout +python3.12 -I -W error -B research/orthogonal-boolean-fanout/verify.py +``` + +Recorded finite coverage: 456 demand triples, 11,400 words, 91,200 formal +forward/inverse column checks, 204,800 literal input checks, all 25 strict +exposures, 81 column-distance queries and ten controls. Five full-state +shortest-path queries settle 90,347 states in total, counted separately by +direction and query; their optima are 3, 6, 6, 14 and 41/15. Controls distinguish +nonorthogonal demands, zero demands, omitted dirt preparation, the wrong +Boolean identity, an invalid per-edge return bound and nonpositive prices. +The registered normal and optimized Python 3.12 runs agree. Three disposable +optimized-mode mutations reject an underpriced one-insertion branch, an +omitted suffix gate and incorrectly forcing the cheapest extra ADDs to use +the insertion row. + +Independent human review and proof-kernel acceptance are unclaimed. +Independently priced directed edges, extra helpers, restricted coefficients, +non-Boolean rings and a complete Pareto census are outside this theorem. +Physical source access, coefficient production, routing, precision, stock +and supplier admission remain separate; the selected frontier is unchanged. + +## Sources and coordination + +Scientific base: canonical main `32890bc5de034ab8fc93ac88ead7279a6a416d04`, +priority revision 7. TASK.json retains the historical `bit-helper-contract` +card and explicitly records the donor-assigned algebraic scope change. +SOURCES.json pins the merged predecessor proof/code bytes at this main base. +No predecessor executable, historical Git object, network or third-party +library is required for direct verifier execution. + +Entry checks on 2026-10-25 covered 371 open PRs (05:34 UTC) and 4,779 +Discussion records (05:37 UTC), both with complete remote pagination, plus +all-state targeted PR searches and current #1166/#5030 reads. No resolving +result or same-scope active claim appeared within that coverage. Sparse +historical notes, arbitrary diffs and unpublished work remain coverage limits. +The public #5030 predecessor leaves this exact question unreserved. +Submission freshness and publication status are recorded with the contribution. + +## Open next questions + +1. Determine the complete aggregate Pareto frontier for this same demand. + Start with eight-ADD one-insertion words having incoming counts + `(3,3,2)` and its permutations, for each insertion row. The + tariff proof permits them but neither constructs nor excludes them; + deciding them separates exposed price-envelope vectors from all Pareto vectors. +2. Determine the tariff with independently priced directed ADD edges. Begin + with a common insertion price, unit prices on a directed three-cycle and + a common positive reverse-edge price. The present row-price column lemma + loses parent identities and cannot by itself supply that lower bound. + +These are suggested next obligations, not reservations or novelty guarantees. +Structured first steps and blockers are in TASK.json. + +## Credit + +Prepared by lee-phys with substantial OpenAI Codex assistance in source +inspection, derivation, implementation, checking and writing. No subagents +or independent reviewers were used. Apache-2.0. The interpreter and full-state +Dijkstra infrastructure are adapted from lee-phys #5304, which adapted #5259; +those packages also supply the insertion-support framework and return lemma. +Credit Ali Romman #5266/#5310 for source-insertion feasibility, 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 support classification and restoring words, Ross Richardson +#3063/#3121 for tariff/restoration arguments, and Cinna Davis, Anthony, +Oscar Fennell, Tekalign and the retained earlier fanout lineage. diff --git a/research/orthogonal-boolean-fanout/SOURCES.json b/research/orthogonal-boolean-fanout/SOURCES.json new file mode 100644 index 0000000000..d321cece65 --- /dev/null +++ b/research/orthogonal-boolean-fanout/SOURCES.json @@ -0,0 +1,49 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/boolean-triple-fanout/README.md", + "usage": "provenance", + "git_blob": "efa6fe83c9081f2895fae16718c44f3c5dad7bde", + "sha256": "8ccfe785fe04f982ab6ee05ac23727f0905cf198d5113d46ca70f553c753fd75" + }, + { + "path": "research/boolean-triple-fanout/verify.py", + "usage": "provenance", + "git_blob": "eeed466cc59c91b3c4f3ce7317fafc7547352f8e", + "sha256": "2193dcb5bfeef751b2346b6c7396040a634a03e0e1ea2ad3546a3b6000431395" + }, + { + "path": "research/square-zero-triple-fanout/README.md", + "usage": "provenance", + "git_blob": "e29c4ef2eb7f365f7b4f9bfa11baf38b2992f9d4", + "sha256": "4e46d3aa0265b79f460c9475f66c3a755c3ed5c1d66a2c6b56cceb8ab0bb7c22" + }, + { + "path": "research/square-zero-triple-fanout/verify.py", + "usage": "provenance", + "git_blob": "cb24a34515c3176106fe763eb9f45c5c09b8006f", + "sha256": "f671e3b8bf702e47111f143fd668ef3f188af8b3d3068ae49859fd19745721c1" + } + ], + "bibliographic_sources": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5310", + "author": "Ali Romman", + "role": "Prior source-insertion count theorem; attribution only, not an executable dependency. The ideal-invariance necessity is proved in the present README." + } + ] +} diff --git a/research/orthogonal-boolean-fanout/TASK.json b/research/orthogonal-boolean-fanout/TASK.json new file mode 100644 index 0000000000..2c3626927b --- /dev/null +++ b/research/orthogonal-boolean-fanout/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "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": "Prove the exact 25-term arbitrary-positive destination-row price envelope for demand (1,2,4) over F2^3, with matching words; extend to nonzero pairwise orthogonal triples over Boolean rings. No complete Pareto census is claimed.", + "scope_change_reason": "Explicit donor assignment of Open next question 2 from #5304; an algebraic side result, not an H2/K replacement or a physical supplier expansion.", + "bottleneck_link": "An exact abstract dirty-input bill; physical access, routing, precision, stock and complete supplier admission remain separate. No new kappa.", + "budget_minutes": 60, + "stop_rule": "Prove the sharp one-insertion bound and complete multi-insertion price envelope; otherwise publish the exact unresolved branch. Bound finite corroboration to small Boolean rings and representative independent shortest paths.", + "outcome": "completed", + "evidence": "README.md supplies an all-word proof. The self-contained verifier checks 456 demands, 11400 words, 91200 formal forward/inverse column checks, 204800 literal input checks, 25 strictly exposed terms, 81 independent weighted column distances, ten controls, and five full-state shortest paths settling 90347 states. Finite evidence is not proof-kernel or independent human acceptance. Registered normal/optimized Python 3.12 replays agree; three disposable optimized-mode mutations reject underpricing, an omitted suffix gate and incorrectly tying the extra ADD destination to the insertion root.", + "author": "lee-phys, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in source inspection, mathematical derivation, implementation, exact experiments, verification and writing; no subagents or independent reviewers.", + "open_questions": [ + { + "question": "What is the complete aggregate Pareto frontier for (1,2,4) over F2^3?", + "why_it_matters": "The exact price envelope need not enumerate unexposed componentwise minimal count vectors.", + "first_step": "Test eight-ADD single-insertion words with incoming counts (3,3,2) and its permutations, allowing any insertion root and all original dirt columns.", + "blocked_by": "The weighted prefix/suffix bound permits these counts but does not construct or exclude them." + }, + { + "question": "What is the exact tariff for the same demand with independent directed-edge prices?", + "why_it_matters": "Destination-only prices do not model arbitrary routing asymmetry.", + "first_step": "Use common source price, unit prices on a directed three-cycle, and one common positive reverse-edge price; preserve the full dirt matrix.", + "blocked_by": "The column proof charges destinations rather than parents; the return lemma is not a universal per-edge bound." + } + ], + "coordination": { + "entry_main": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "open_prs": 371, + "open_prs_fetched_at": "2026-10-25T05:34:59.494702+00:00", + "discussion_records": 4779, + "discussions_fetched_at": "2026-10-25T05:37:23.777879+00:00", + "complete_remote_pagination": true, + "supplement": "All-state Boolean/fanout PR searches, current #1166/#5030 reads and predecessor Open next questions. No resolving same-scope result or active claim found. Sparse historical notes and arbitrary diffs not exhaustively searched.", + "public_claim": null + } +} diff --git a/research/orthogonal-boolean-fanout/VERIFY.json b/research/orthogonal-boolean-fanout/VERIFY.json new file mode 100644 index 0000000000..fdba41165f --- /dev/null +++ b/research/orthogonal-boolean-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": 180, + "checks": "Exact Boolean-ring constructors/inverses, 25 strict price witnesses, weighted column Dijkstra, full dirt-state Dijkstra and failure controls; normal mode." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact Boolean-ring constructors/inverses, 25 strict price witnesses, weighted column Dijkstra, full dirt-state Dijkstra and failure controls; optimized mode." + } + ] +} diff --git a/research/orthogonal-boolean-fanout/verify.py b/research/orthogonal-boolean-fanout/verify.py new file mode 100644 index 0000000000..e4ab0df938 --- /dev/null +++ b/research/orthogonal-boolean-fanout/verify.py @@ -0,0 +1,388 @@ +#!/usr/bin/env python3 +"""Exact bounded checks for the orthogonal Boolean triple tariff; Apache-2.0. + +lee-phys with substantial OpenAI Codex assistance. Adapted word, interpreter +and Dijkstra infrastructure from #5304 (c8bf34c359b3a12f112078f0072b4ecc7a942109), +which adapted #5259 (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 i in range(3): + for h in range(3): + v = [0, 0, 0, 2, 2, 2] + v[i], v[3+h] = 1, 4 + out.append(('U', i, h, -1, tuple(v))) + return out + + +def construct(r, d, pattern): + mode, i, j, k, _ = pattern + g = r.add[r.add[d[0]][d[1]]][d[2]] + if mode == 'D': + return [(t, 3, d[t]) for t in range(3)] + if mode == 'T': + return [(j, i, d[j]), (i, 3, g), (j, i, d[j]), + (k, i, d[k]), (i, 3, r.add[g][d[i]]), (k, i, d[k])] + if mode == 'R': + return [(k, i, d[k]), (i, 3, r.add[d[i]][d[k]]), (k, i, d[k]), + (i, 3, d[k]), (j, 3, d[j])] + if mode == 'M': + suffix = [(k, i, d[k]), (i, k, d[k])] + return inverse(r, suffix)+[(i, 3, r.add[d[i]][d[k]])]+suffix+[(j, 3, d[j])] + if mode == 'U': + h = j + j, k = [t for t in range(3) if t != i] + if h == i: + suffix = [(j,i,d[j]), (k,i,d[k]), (i,j,d[j]), (i,k,d[k])] + else: + j, k = h, next(t for t in range(3) if t not in (i,h)) + q = r.add[d[j]][d[k]] + suffix = [(j,i,q), (k,i,d[k]), (i,j,q), (j,k,d[k])] + 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 any(x == 0 for x in d): + raise ValueError('nonzero demands required') + if any(r.mul[d[i]][d[j]] != 0 for i,j in permutations(range(3),2)): + raise ValueError('pairwise orthogonal demands 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)+2*min(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])) + return min(out) + + +def column_oracle(root, prices): + # Independent all-ADD Dijkstra on the complete source-column orbit. + # This is a projection, not a substitute for the full dirt-state oracle. + start, goal = 7 << (3*root), 1 | (2 << 3) | (4 << 6) + ds, q = {start: 0}, [(0,start)] + while q: + distance, state = heappop(q) + if distance != ds[state]: + continue + if state == goal: + return distance + rows = [(state >> (3*i)) & 7 for i in range(3)] + for i,j in permutations(range(3),2): + for coefficient in range(1,8): + target = state ^ ((rows[j] & coefficient) << (3*i)) + cost = distance+prices[i] + if target not in ds or cost < ds[target]: + ds[target] = cost + heappush(q,(cost,target)) + raise RuntimeError('column endpoints disconnected') + + +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)) == 25, 'twenty-five distinct exposed vectors') + total = dict(demands=0, words=0, formal_forward_inverse=0, literal_forward_inverse=0, + exposed_vectors=0, column_queries=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 d in product(range(1,r.n),repeat=3): + if any(r.mul[d[i]][d[j]] != 0 for i,j in permutations(range(3),2)): + continue + validate_demand(r,d) + g = r.add[r.add[d[0]][d[1]]][d[2]] + 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') + for i,j,k in permutations(range(3)): + require(d[k] not in r.ideal((d[i],d[j])), 'absent two-parent demand component') + 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, 'three disjoint nonempty supports') + total['demands'] += accepted + fixtures.append(dict(ring=r.name,demands=accepted,proper_ideal_demands=proper)) + + r, d = boolean_ring(3), (1,2,4) + 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), (5,9,9,1,2,2), (7,12,12,2,1,2)] + 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-five-term envelope') + exposed.add(costs.index(minimum)) + require(len(exposed) == 25, 'every listed term 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+8*c), 'uniform-price corollary') + for prices in product(range(1,4),repeat=3): + for root in range(3): + require(column_oracle(root,prices) == sum(prices)+min(prices), + 'independent weighted source-column distance') + total['column_queries'] += 1 + + # A zero-sum witness costs 16 but cannot realize the new demand at that bill. + p = (10,100,100,1,1,1) + old = [(0,1,4),(2,0,6),(1,0,5),(0,3,7),(1,0,5),(2,0,6),(0,1,4)] + require(endpoint(r,(3,5,6),old) and bill(old,p) == 16 < formula(p[:3],p[3:]) == 18, + 'zero-sum and orthogonal demands have different tariffs') + require(not endpoint(r,d,old), 'old word does not solve the assigned endpoint') + total['controls'] += 1 + for bad, fragment in [((1,2,0),'nonzero'), ((3,5,6),'orthogonal'), ((1,1,4),'orthogonal')]: + 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') + corrupted = words[16][4:] + 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[16]] + 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 + 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'),representatives[:4])) + 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(dict(case=name,optimum=str(value),settled=settled)) + print('CHECK_ORACLE',name,str(value),flush=True) + print(json.dumps(dict(fixtures=fixtures,counts=total,oracle=results),sort_keys=True)) + print('PASS_ORTHOGONAL_BOOLEAN_FANOUT no_new_kappa') + + +if __name__ == '__main__': + main()