diff --git a/research/square-zero-triple-fanout/README.md b/research/square-zero-triple-fanout/README.md new file mode 100644 index 0000000000..e29c4ef2eb --- /dev/null +++ b/research/square-zero-triple-fanout/README.md @@ -0,0 +1,301 @@ +# Exact dirty-fanout tariff for a nonprincipal zero-sum triple + +**Scoped written proof with exact finite corroboration; no new kappa.** +For three arbitrary dirty rows over +`R=F2[e,h]/(e^2,eh,h^2)` with demand `(e,h,e+h)`, the exact +positive-price envelope has **19 indispensable terms**. All 19 aggregate +count vectors are attained and form the complete Pareto frontier. + +This resolves the unequal all-nonunit example in lee-phys +[#5163](https://github.com/CrocSwap/integer-mult-bounds/pull/5163) and Nick Petalas +[#5208](https://github.com/CrocSwap/integer-mult-bounds/pull/5208). +The proof also applies over every commutative unital ring to every zero-sum +triple generating a nonprincipal ideal. Finiteness, locality and a square-zero +radical are unnecessary for this extension. + +## Contract and price formula + +Let R be a commutative ring with `1 != 0`. There are exactly three independent +arbitrary dirty rows `a_0,a_1,a_2 in R^w`, w >= 1, and one disjoint preserved +source p. A fixed finite straight-line word must produce + + A_i = a_i + lambda_i p, i=0,1,2, + +while retaining all original dirt. 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. + +Every coefficient and ordered pair is available. Prices are finite, +stationary, coefficient-independent complete abstract prices; an ADD price +depends only on its receiving row. Zero-coefficient gates may be deleted. +There are no extra rows, clearing, observations, adaptive choices or free +basis changes. A separate inverse execution has a separate bill. + +**Theorem.** Suppose + + lambda_0 + lambda_1 + lambda_2 = 0, + I = (lambda_0,lambda_1,lambda_2) is not a principal ideal. + +For `{i,j,k}={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,2c_k). + +Then the exact optimum over all allowed words is + + OPT = min(D,T_0,T_1,T_2,B_0,B_1,B_2). + +Expanding each B_k gives nineteen linear terms. Every term is necessary for +some strictly positive price vector. The formula requires a constant number +of arithmetic/comparison operations once prices and the algebraic hypotheses +are supplied. It does not price determining ideal structure or implementing +the abstract gates physically. + +For the requested eight-element ring, `I=(e,h)={0,e,h,e+h}` is nonprincipal: +a nonunit generator x has `(x)={0,x}`, whereas a unit generates R. The +zero-sum identity holds in characteristic two. Thus the theorem applies. +At mu=(1,9,9), c=(1,1,1), the exact optimum is **6**, attained by + + E_10(1), P_0(h), E_10(1), + E_20(1), P_0(e+h), E_20(1). + +The first echo gives row 1 its demand h, the second gives row 2 its demand +e+h, and the two insertions leave e in row 0. In contrast, the equal-demand +example `(e,e,e)` has cost five at these prices, as covered by #5208. Equality +of the demands is an essential distinction. + +## Lower bound for arbitrary interleavings + +### Two necessary facts + +First, the hypotheses imply every lambda_i is nonzero and +`lambda_i not in (lambda_j)` whenever i != j. Indeed, if +`lambda_i in (lambda_j)`, the zero-sum relation puts the third demand in +`(lambda_j)` as well, making I principal. If a demand is zero, the remaining +two are negatives and again generate a principal ideal. + +At least two nonzero P calls are necessary. With exactly one call P_r(beta), +the final source coefficient column is `beta v`, where v is column r of the +invertible suffix dirt matrix L. Its entries generate exactly `(beta)`: +one inclusion is immediate, and row r of `L^-1` expresses beta as a linear +combination of the final source coefficients. This contradicts nonprincipality +of I. With no P calls the source column is zero. This is the ideal-invariance +necessity from #5139, applied to three rows; no sufficiency claim is used. + +Second, a row cannot receive exactly one nonzero ADD while its original dirt +returns. Let M be the invertible dirt matrix immediately before that sole +`E_ij(alpha)`. Row i has remained e_i, and the update changes it to +`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. +Consequently every row with no P call must receive at least two ADDs, since +its nonzero final source coefficient otherwise remains zero. This is the +credited incoming-row return argument of #3063/#4916/#5163. + +The argument concerns total incoming calls, not each individual edge. The +verifier retains the three-row five-ADD identity from #5163 as a control +against that invalid stronger interpretation. + +### Classify by insertion support + +Let S be the set of rows receiving at least one nonzero P call. Charge each +gate to its destination, and write K_i for the total number of incoming ADDs. + +If S contains all three rows, the bill is at least D. If `S={i}`, at least +two P_i calls and two ADDs into each other row are needed. The bill is at +least T_i, regardless of coefficients or interleavings. + +It remains to consider `S={i,j}`, with k the row without insertions. In all +cases `K_k>=2`. + +* If either i or j receives a second P call, the bill is at least + `mu_i+mu_j+2c_k+min(mu_i,mu_j)`. +* Otherwise there is exactly one insertion in each of i,j. If either of these + rows receives any ADD, it receives at least two, giving the lower bound + `mu_i+mu_j+2c_k+min(2c_i,2c_j)`. +* Otherwise neither insertion row receives an ADD. Their dirt rows stay + a_i,a_j throughout, and their single inserted coefficients are respectively + lambda_i,lambda_j. To produce lambda_k, row k must use both incoming + edges: either parent alone could produce only an element of its principal + ideal. On each used edge, the sum of its coefficients must be zero to + restore that parent's independent dirt. A single nonzero call cannot have + zero sum, so each edge occurs at least twice. Thus `K_k>=4`, giving + `mu_i+mu_j+4c_k`. + +The last per-edge count is used only when both parent dirt rows are unchanged. +Taking the minimum of these exhaustive cases gives B_k. Together the cases +prove the stated all-word lower bound. Repeated insertions, unit insertions +with cancellations, feedback and arbitrary finite interleavings are included. + +## Matching words and the nineteen count vectors + +All words are chronological. Indices i,j,k below are distinct. Signed +coefficients are retained so the same constructions work in odd characteristic. +Let a count vector record `(P_0,P_1,P_2,K_0,K_1,K_2)`. + +| Family | Price | Nonzero counts | Number | +|---|---|---|---| +| D | `sum mu_i` | `P_i=1` for all i | 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 | + +**D: direct insertion.** Use `P_i(lambda_i)` on all three rows. + +**T_i: two successive echoes from one insertion row.** Use + + E_ji(1), P_i(-lambda_j), E_ji(-1), + E_ki(1), P_i(-lambda_k), E_ki(-1). + +Each echo transfers the increment between its two row gates. The second +preparation includes the source coefficient already present in row i; that +coefficient cancels on undoing the preparation. Row i ends with +`-lambda_j-lambda_k=lambda_i`, and each other row receives its own demand. + +**R_(i,j;k): repeat one root and insert directly into the other.** Use + + E_ki(1), P_i(-lambda_k), E_ki(-1), + P_i(-lambda_j), P_j(lambda_j). + +The echo gives lambda_k to k. The two P_i calls sum to lambda_i; the direct +P_j call supplies lambda_j. No dirt remains mixed. + +**M_(i,j;k): prepare a two-edge chain.** Use + + E_ij(1), E_ki(1), P_i(-lambda_k), P_j(lambda_j), + E_ki(-1), E_ij(-1). + +Just before undoing the preparation, the three relevant 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. + +The last two gates give A_k its required increment lambda_k p and give A_i +`(-lambda_k-lambda_j)p=lambda_i p`, restoring all dirt. + +**Q_k: combine two independent source rows.** Use + + E_ki(1), E_kj(1), P_i(lambda_i), P_j(lambda_j), + E_kj(-1), E_ki(-1). + +The final increment at k is `(-lambda_i-lambda_j)p=lambda_k p`. +All gates above have nonzero coefficients. Their exact counts match the table. +Literal inversion reverses the word and negates every coefficient. + +The lower-bound classification proves that every achievable count vector +componentwise dominates at least one table vector. These nineteen vectors +are pairwise incomparable and all attained, so they are exactly the Pareto +frontier. To show each is also indispensable for strictly positive prices, +it suffices to expose one representative of each family; permute row labels +for the other cases. Prices below are in `(mu_0,mu_1,mu_2,c_0,c_1,c_2)` order: + +| Unique minimum | Positive price vector | Optimum | +|---|---|---| +| 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 | + +## Hypotheses and verification + +Nonprincipality is substantive. In the Boolean product ring `F2 x F2 x F2`, +write elements as bit masks, with identity 7. Demand `(3,5,6)` has sum zero +and pairwise incomparable principal ideals, but generates the principal unit +ideal. Set + + L = E_10(5), E_20(6), E_01(4). + +Starting from column `(7,0,0)`, L produces `(3,5,6)`. Therefore the chronological +word `L^-1, P_0(7), L` meets the dirty endpoint. It costs 16 at +mu=(10,100,100), c=(1,1,1), below the inapplicable formula's value 24. +The verifier checks this strict discriminator. It is not a claim of the full +Boolean-ring optimum. Nonzero demand lists failing the zero-sum condition +are also outside the theorem. + +The self-contained standard-library verifier checks all nineteen words and +inverses on every formal input column over four finite rings: the requested +ring, its odd-characteristic F3 counterpart, `Z/4[t]/t^2`, and the nonlocal +product of the requested ring with F2. It enumerates all zero-sum demand +triples generating nonprincipal ideals in those fixtures. Literal scalar +checks cover every input assignment for all nineteen requested-ring words. +Exact count vectors, strict positive-price exposure and hypothesis-removal +controls are checked separately. + +A separate packed-state bidirectional Dijkstra oracle searches unrestricted +three-row words over the requested eight-element ring. It tracks all nine +dirt and three source coefficients, permits every nonzero gate coefficient +and every directed edge, and uses no word-length cutoff or formula pruning. +Its two frontier lower bounds certify the best meeting distance. Returned +words are replayed and charged by the primary ring interpreter. The search +explores implicit finite states; it does not enumerate the entire affine graph. +The verifier prints exact coverage and search counts. + +The recorded run covers 102 demand triples and 1,938 words, with 15,504 +formal forward/inverse column checks and 155,648 literal scalar checks. +Seven oracle queries settle 129,443 states in total (counted separately in +each search direction and query). The five family witnesses have exact costs +3, 6, 6, 14 and 10; the asymmetric example costs 6, and the rational-price +case costs 79/30. Normal and optimized isolated Python runs have identical +complete output. Three disposable optimized-mode mutations are rejected: +undercharging the two-insertion term, omitting a chain's dirt preparation, +and replacing heterogeneous oracle prices by unit weights. + +```sh +python3.12 -B scripts/research_package.py --package research/square-zero-triple-fanout --check-only +python3.12 -B scripts/research_package.py --package research/square-zero-triple-fanout +python3.12 -I -W error -B research/square-zero-triple-fanout/verify.py +``` + +The arbitrary-ring and all-positive-price statements rest on the written proof; +finite checks corroborate bounded cases. Independent human review and +proof-kernel acceptance are unclaimed. Physical source access, coefficient +preparation, routing, precision, stock and complete supplier admission remain +outside this complete abstract-price contract. No selected-frontier change +or new kappa follows. + +## Sources and overlap + +Scientific base: canonical main `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, +priority revision 7. TASK.json preserves the historical `bit-helper-contract` +card and records the explicit donor's algebraic side-result scope change. +SOURCES.json pins the predecessor proof texts as provenance; no predecessor +executable is imported. + +The immediately preceding survey covered 311 open PRs at 13:54 UTC and 4,490 +Discussion records at 13:58 UTC on 2026-10-23, with complete reported remote +pagination. New all-state targeted PR searches and live #5030/#1166 reads at +entry found no resolving successor. Sparse historical notes, arbitrary diffs +and unpublished work were not exhaustively searched. Submission refresh and +hosted CI are recorded in the PR. + +## Open next questions + +1. Price a zero-sum triple with a principal demand ideal and incomparable + component ideals, beginning with `(3,5,6)` over the Boolean product ring. + One-insertion words can now compete, so the source-support lower bound + needs a new one-insertion branch; the cost-16 discriminator is only an upper + bound for that case. +2. Determine independently directed-edge-priced tariffs for the requested + `(e,h,e+h)` triple. Start with a cheap directed cycle. Destination totals + discard the identities of incoming parents and do not provide its lower bound. +3. Classify nonprincipal triples without the zero-sum relation, beginning with + `(e,h,e+h+z)` in `F2[e,h,z]/(e,h,z)^2`. Its demand ideal needs three generators, and the zero-sum constructions + no longer supply the target. Cancelling unit insertions must still be + considered when seeking a lower bound. + +## Credit + +Prepared by lee-phys with substantial OpenAI Codex assistance in derivation, +implementation, checking and writing; no subagents or independent reviewers. +Apache-2.0. Credit Nick Petalas #5208 for the equal-demand theorem and explicit +unequal-demand handoff, lee-phys #5139/#5163 for ideal invariance and the local-ring +boundary, Krzysztof Wojt #5045 for source-count classification and two-row +restoring words, Nick Petalas #4916 for the ring-valued contract, Ross Richardson +#3063/#3121 for tariff and dirt-restoration arguments, and Cinna Davis, Anthony, +Oscar Fennell, Tekalign and the retained lineage. The new step is the exhaustive +two-recipient surcharge and its matching nineteen-vector zero-sum frontier. diff --git a/research/square-zero-triple-fanout/SOURCES.json b/research/square-zero-triple-fanout/SOURCES.json new file mode 100644 index 0000000000..4e5757f2b4 --- /dev/null +++ b/research/square-zero-triple-fanout/SOURCES.json @@ -0,0 +1,42 @@ +{ + "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" + }, + { + "path": "research/equal-nonunit-fanout/README.md", + "usage": "provenance", + "git_blob": "f97c05717fbdcb1b1675f23ca8eee79e27147111", + "sha256": "e90435ecd273fa028ba29ad83f0a7dca89661ff86c695b44030401a7ef773af2" + }, + { + "path": "research/two-row-nonunit-fanout/PROOF.md", + "usage": "provenance", + "git_blob": "1bd3b47624db83c45ca08fb498f2a84d814306c1", + "sha256": "d177967c73bd5e755c5f70964d5542420e23e36cad81c57452a222e50e356f77" + } + ] +} diff --git a/research/square-zero-triple-fanout/TASK.json b/research/square-zero-triple-fanout/TASK.json new file mode 100644 index 0000000000..d9501cf303 --- /dev/null +++ b/research/square-zero-triple-fanout/TASK.json @@ -0,0 +1,73 @@ +{ + "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 positive destination-row tariff for dirty three-row demand (e,h,e+h) over F2[e,h]/(e,h)^2, and prove the resulting nineteen-vector frontier for nonprincipal zero-sum triples over commutative unital rings.", + "scope_change_reason": "The donor explicitly assigned this algebraic problem after the merged two-row and local-ring boundary work. It is a scoped side result, not a replacement H2/K interface or an extension of an admitted bit supplier.", + "bottleneck_link": "Provides a rigorously priced dirty-input identity and all-word lower bound in a complete abstract gate-price model. Applying it to a physical supplier still requires source access, coefficient, routing, precision, stock and full interface accounting; no selected-kappa improvement is claimed.", + "budget_minutes": 60, + "stop_rule": "Finish when all price terms have matching words and an all-interleaving lower bound, or record a precise unresolved branch or counterexample within the 60-minute session. Restrict finite corroboration to four small rings and seven independent eight-element shortest-path cases.", + "outcome": "completed", + "evidence": "README.md proves the nineteen-vector Pareto frontier and exact arbitrary-positive-price envelope. The self-contained verifier checks 102 demand triples in four rings, 1,938 matching words, 15,504 formal forward/inverse column checks, 155,648 literal input checks, strict exposure of all 19 vectors, eight controls and seven independent packed-state shortest paths. Finite checks corroborate the written proof; human review, proof-kernel acceptance and physical supplier admission are unclaimed.", + "author": "lee-phys, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in source inspection, derivation, construction, Python implementation, finite experiments, verification and writing. No subagents or independent reviewers were used.", + "open_questions": [ + { + "question": "What is the exact destination-row tariff for demand (3,5,6) in the Boolean product ring F2 x F2 x F2?", + "why_it_matters": "The demand is zero-sum with incomparable component ideals but a principal total ideal. A verified one-insertion word beats the present formula, so a separate branch is necessary.", + "first_step": "Enumerate and bound one-insertion restoring words, starting from the cost-16 word in README.md, then compare their envelope with multi-insertion words.", + "blocked_by": "The nonprincipal-ideal lower bound on the number of source calls does not apply; the cost-16 witness is only an upper bound." + }, + { + "question": "What is the exact tariff for (e,h,e+h) over the eight-element ring when every directed ADD edge has its own positive price?", + "why_it_matters": "Destination totals can conceal a cheaper sequence using a directed cycle and do not determine edge-sensitive optimality.", + "first_step": "Use a cheap directed three-cycle as a finite shortest-path probe and classify the source-support cases with edge counts retained.", + "blocked_by": "A per-edge two-call restoration lemma is false for three rows, as the retained five-ADD identity demonstrates." + }, + { + "question": "What is the exact tariff for the non-zero-sum demand (e,h,e+h+z) in F2[e,h,z]/(e,h,z)^2?", + "why_it_matters": "The demand ideal needs three generators and the zero-sum constructions no longer reach the endpoint; cancelling unit insertions must still be considered.", + "first_step": "Find matching words for the cheapest insertion-support cases and test small positive-price regimes with full dirt tracking.", + "blocked_by": "The present theorem uses the zero-sum identity for all four indirect construction families and makes no claim about this demand." + } + ] +} diff --git a/research/square-zero-triple-fanout/VERIFY.json b/research/square-zero-triple-fanout/VERIFY.json new file mode 100644 index 0000000000..ef065bcb30 --- /dev/null +++ b/research/square-zero-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": 180, + "checks": "Normal exact four-ring constructors and inverses, 19 exposed count vectors, all scalar eight-element inputs, eight hypothesis/dirty-input controls and seven unrestricted packed-state shortest paths; no new kappa." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Optimized exact four-ring constructors and inverses, 19 exposed count vectors, all scalar eight-element inputs, eight hypothesis/dirty-input controls and seven unrestricted packed-state shortest paths; no new kappa." + } + ] +} diff --git a/research/square-zero-triple-fanout/verify.py b/research/square-zero-triple-fanout/verify.py new file mode 100644 index 0000000000..cb24a34515 --- /dev/null +++ b/research/square-zero-triple-fanout/verify.py @@ -0,0 +1,358 @@ +#!/usr/bin/env python3 +"""Exact bounded checks for README.md; no new kappa. + +lee-phys with substantial OpenAI Codex assistance; Apache-2.0. +Retains #5045/#5139/#5163/#5208 and the credited fanout lineage. +""" +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 square_zero(p): + def digits(x): + return (x % p, (x//p) % p, x//(p*p)) + def add(x, y): + a, b = digits(x), digits(y) + return sum(((a[k]+b[k]) % p)*p**k for k in range(3)) + def mul(x, y): + a, b = digits(x), digits(y) + return a[0]*b[0] % p + p*((a[0]*b[1]+a[1]*b[0]) % p) + p*p*((a[0]*b[2]+a[2]*b[0]) % p) + return ring_from_functions(f'F{p}[e,h]/(e,h)^2', p**3, 1, add, mul) + + +def dual_z4(): + return ring_from_functions('Z/4[t]/t^2', 16, 1, + lambda x, y: (x % 4+y % 4) % 4+4*((x//4+y//4) % 4), + lambda x, y: (x % 4)*(y % 4) % 4+4*(((x % 4)*(y//4)+(x//4)*(y % 4)) % 4)) + + +def product_ring(eight): + return ring_from_functions('F2[e,h]/(e,h)^2 x F2', 16, 9, + lambda x, y: eight.add[x % 8][y % 8]+8*((x//8+y//8) % 2), + lambda x, y: eight.mul[x % 8][y % 8]+8*((x//8)*(y//8))) + + +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 validate_demand(r, d): + if len(d) != 3 or any(not isinstance(x, int) or x not in range(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 r.ideal(d) in {r.principal(x) for x in range(r.n)}: + raise ValueError('the generated ideal must be nonprincipal') + + +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)] + 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 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))) + 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)] + 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) + + +# Independent eight-element implementation: 12-bit rows, 36-bit affine states. +# No constructor, price formula, ideal routine or ring table is called here. +def packed_tables(): + return [None]+[tuple(sum((((a & 1)*((x >> (3*k)) & 7)) ^ + (((x >> (3*k)) & 1)*(a & 6))) << (3*k) for k in range(4)) + for x in range(4096)) for a in range(1, 8)] + + +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 = 1 | (8 << 12) | (64 << 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 main(): + eight = square_zero(2) + pats = patterns() + vectors = [p[-1] for p in pats] + require(len(vectors) == len(set(vectors)) == 19, 'nineteen distinct count 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 r in (eight, square_zero(3), dual_z4(), product_ring(eight)): + check_ring(r) + principal_ideals = {r.principal(x) for x in range(r.n)} + accepted = 0 + for a, b in product(range(r.n), repeat=2): + d = (a, b, r.neg(r.add[a][b])) + if r.ideal(d) in principal_ideals: + continue + validate_demand(r, d) + require(all(x != 0 for x in d), 'nonprincipal zero-sum demands are nonzero') + require(all(d[i] not in r.principal(d[j]) for i in range(3) for j in range(3) if i != j), + 'pairwise principal incomparability') + accepted += 1 + for pattern in pats: + word = construct(r, d, pattern) + require(all(a != 0 for _, _, a in word), 'exact-price words have no zero 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 + total['demands'] += accepted + fixtures.append({'ring': r.name, 'zero_sum_nonprincipal_triples': accepted}) + + d = (2, 4, 6) + words = [construct(eight, d, p) for p in pats] + for word in words: + rev = inverse(eight, word) + for entry in product(range(8), repeat=4): + want = target(eight, d, entry) + require(execute(eight, word, entry) == want and execute(eight, rev, want) == entry, + 'literal eight-element endpoint/inverse') + total['literal_forward_inverse'] += 2 + + representative_prices = [(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)] + exposed = set() + for prices in representative_prices: + 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 nineteen-term envelope') + exposed.add(costs.index(minimum)) + require(len(exposed) == 19, 'every vector exposed by positive prices') + total['exposed_vectors'] = len(exposed) + + # A one-insertion discriminator when the nonprincipal-ideal hypothesis is dropped. + boolean = ring_from_functions('F2 x F2 x F2', 8, 7, lambda x, y: x ^ y, lambda x, y: x & y) + check_ring(boolean) + bd = (3,5,6) + suffix = [(1,0,5), (2,0,6), (0,1,4)] + one_call = inverse(boolean, suffix)+[(0,3,7)]+suffix + prices = (10,100,100,1,1,1) + require(endpoint(boolean, bd, one_call), 'principal-ideal one-insertion discriminator') + require(bill(one_call, prices) == 16 < formula(prices[:3], prices[3:]) == 24, + 'nonprincipality is essential') + total['controls'] += 1 + for ring, demand, fragment in [(boolean, bd, 'nonprincipal'), (eight, (2,4,2), 'sum to zero')]: + try: + validate_demand(ring, demand) + except ValueError as error: + require(fragment in str(error), 'correct domain rejection') + total['controls'] += 1 + else: + raise RuntimeError('accepted demand outside the theorem') + bad_sum_word = construct(eight, (2,4,2), pats[1]) + require(not endpoint(eight, (2,4,2), bad_sum_word), 'zero-sum hypothesis is substantive') + total['controls'] += 1 + corrupted = words[1][1:] + require(execute(eight, corrupted, (0,0,0,1)) == (*d,1), 'dirty-only corruption premise') + require(not endpoint(eight, d, corrupted), 'reject missing dirt preparation') + total['controls'] += 1 + relator = [(0,1,1), (1,2,1), (0,1,1), (1,2,1), (0,2,1)] + require(endpoint(eight, (0,0,0), relator), 'single-edge identity control') + require(sum((i,j) == (0,2) for i,j,_ in relator) == 1, 'no universal per-edge return lemma') + total['controls'] += 1 + 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 tariff') + + tables = packed_tables() + cases = list(zip(('D','T','R','M','Q'), representative_prices)) + cases += [('cheap-root', (1,9,9,1,1,1)), + ('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(eight, d, path) and bill(path, prices) == value, 'oracle word replay and tariff') + 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_SQUARE_ZERO_TRIPLE_FANOUT no_new_kappa') + + +if __name__ == '__main__': + main()