From cdd7714c20352f7106f005066c3ed65534e98516 Mon Sep 17 00:00:00 2001 From: lizhi Date: Fri, 23 Oct 2026 19:22:05 +0800 Subject: [PATCH] Prove destination-priced nonunit dirty-fanout tariffs over local rings --- research/local-ring-row-fanout/README.md | 334 ++++++++++++++++++ research/local-ring-row-fanout/SOURCES.json | 36 ++ research/local-ring-row-fanout/TASK.json | 73 ++++ research/local-ring-row-fanout/VERIFY.json | 34 ++ research/local-ring-row-fanout/verify.py | 369 ++++++++++++++++++++ 5 files changed, 846 insertions(+) create mode 100644 research/local-ring-row-fanout/README.md create mode 100644 research/local-ring-row-fanout/SOURCES.json create mode 100644 research/local-ring-row-fanout/TASK.json create mode 100644 research/local-ring-row-fanout/VERIFY.json create mode 100644 research/local-ring-row-fanout/verify.py diff --git a/research/local-ring-row-fanout/README.md b/research/local-ring-row-fanout/README.md new file mode 100644 index 0000000000..a65ecdb615 --- /dev/null +++ b/research/local-ring-row-fanout/README.md @@ -0,0 +1,334 @@ +# Exact destination-priced dirty fanout over local rings + +**Scoped written proof and exact finite corroboration; no new κ.** +For three dirty rows over Z/4 with demand `(2,1,1)`, we determine the exact +optimum for every positive source price and every positive **destination-only** +ADD price. There are eight indispensable price terms. The proof extends to +any number of rows over any commutative local ring, provided at least one +demand is a unit; other demands may be nonunits or zero. + +This takes the three-row question in Krzysztof Wójt's +[#5045](https://github.com/CrocSwap/integer-mult-bounds/pull/5045) and +[#5139](https://github.com/CrocSwap/integer-mult-bounds/pull/5139) to a complete +price family. Independently pricing all six directed ADD edges remains open. +The source-count method and two-row mixing/repeated-insertion words retain +#5045's credit. The additional argument charges the first necessary unit +insertion somewhere among rows with nonunit demands. + +## Contract and the three-row answer + +For q >= 1 arbitrary independent dirty rows `a_i in R^w`, w >= 1, and one +preserved disjoint source `p in R^w`, require `A_i=a_i+lambda_i p` for every i. +Only fixed finite straight-line words in the following gates are allowed: + + 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 prices are finite, stationary, coefficient-independent complete abstract +prices. The ADD price depends on its **destination i**, equally for every +source j. Both directions, all nonzero coefficients and all ordered pairs +are available. All original dirt must return exactly. There are no extra +rows, clearing, free basis changes, observations or adaptive choices. An +inverse execution, when required, is separately charged. Delete any +zero-coefficient gates, since their prices are positive. + +**Three-row theorem.** Over Z/4, for demand `(2,1,1)`, the optimum is the +minimum of the following eight linear expressions, for all positive real +`(mu_0,mu_1,mu_2,c_0,c_1,c_2)`: + +| Name | Price | Counts `(P_0,P_1,P_2,K_0,K_1,K_2)` | +|---|---|---| +| D | `mu_0+mu_1+mu_2` | `(1,1,1,0,0,0)` | +| F01 | `mu_0+mu_1+2c_2` | `(1,1,0,0,0,2)` | +| F02 | `mu_0+mu_2+2c_1` | `(1,0,1,0,2,0)` | +| F12 | `mu_1+mu_2+2c_0` | `(0,1,1,2,0,0)` | +| F1 | `mu_1+2c_0+2c_2` | `(0,1,0,2,0,2)` | +| F2 | `mu_2+2c_0+2c_1` | `(0,0,1,2,2,0)` | +| T0 | `2mu_0+2c_1+2c_2` | `(2,0,0,0,2,2)` | +| S0 | `mu_0+2c_0+2c_1+2c_2` | `(1,0,0,2,2,2)` | + +Here K_i counts **all** ADD calls into row i. These eight vectors form the +exact Pareto frontier for these six aggregate counts. In the table's price +order, each term is uniquely cheapest at the corresponding vector below: + + D: (1,1,1,1,1,1) F01: (1,1,20,10,10,1) + F02: (1,20,1,10,1,10) F12: (20,1,1,1,10,10) + F1: (20,1,20,1,10,1) F2: (20,20,1,1,1,10) + T0: (1,20,20,10,1,1) S0: (5,20,20,1,1,1). + +For example, take mu=(1,9,9) and every directed +ADD price equal to one. The exact optimum is **6**, attained chronologically by + + E_10(-1), E_20(-1), P_0(1), E_20(1), E_10(1), P_0(1). + +A unit-forest relaxation would incorrectly predict five. With mu=(100,1000,1000) +and all ADD prices one, the optimum instead is **106**, attained by + + E_21(-1), E_01(-1), E_10(-1), P_0(1), + E_10(1), E_01(1), E_21(1). + +The middle two-row word gives demands (2,1) on rows 0,1; the outer echo +restores row 2 with demand one. Every dirt column is retained throughout. + +## Arbitrary-row local-ring theorem + +Let R be a commutative local ring with `1 != 0`; finiteness is unnecessary. +Its nonunits form its unique maximal ideal m. Let + + U = {i : lambda_i is a unit}, N = {0,...,q-1} minus U. + +Assume U is nonempty. Zero demands are allowed in N. Define + + a_i = 0 if lambda_i = 0, + min(mu_i,2c_i) otherwise; + A = sum_i a_i, + B = 2 sum_(i in U) c_i + sum_(i in N) a_i. + +For each r in U and each r in N, respectively, define + + F_r = A + mu_r - a_r, r in U; + T_r = B + 2mu_r - a_r, r in N; + S_r = B + mu_r + 2c_r - a_r, r in N. + +**Theorem.** The exact optimum over every allowed finite word is + + OPT = min( min_(r in U) F_r, + min_(r in N) T_r, + min_(r in N) S_r ), + +where a minimum over the empty set is +infinity. Every candidate has an +explicit attaining word. This needs only O(q) arithmetic/comparison operations +once the unit/zero statuses and gate prices are supplied; it does not price +computing that algebraic information or physically implementing the gates. + +Equivalently, the last two minima combine as + + B + min_(r in N) [mu_r + min(mu_r,2c_r) - a_r]. + +If all demands are nonzero, this simplifies further to + + OPT = min(A + min_(r in U)(mu_r-a_r), + B + min_(r in N) mu_r). + +For all-unit demands, N is empty and this recovers the credited +Ross Richardson #3063 / Nick Petalas #4916 destination-price specialization. +At zero total demand, the empty word costs zero. A nonzero demand list with +U empty is outside this theorem, even if its generated ideal is principal. + +## Proof of the all-word lower bound + +### Incoming-row return lemma + +Let M be the matrix of the q original dirt coefficients. It starts and ends +at I_q, and every prefix is invertible: each ADD has its negated-coefficient +inverse, while P calls leave M unchanged. The all-input contract implies +matrix equality by testing each original input coordinate in turn. + +A row cannot receive exactly one nonzero ADD. Before its sole ADD into i, +its dirt row is e_i. Immediately after `E_ij(alpha)` it is `e_i+alpha m_j`, +where m_j is row j of the invertible prefix matrix. No later gate changes +row i's dirt, so restoration would force `alpha m_j=0`. Multiplying by the +prefix inverse gives `alpha e_j=0`, hence alpha=0, a contradiction. Thus +any used destination receives at least two ADDs. This is the singleton +free-module return argument underlying #3063/#4916, restated here. + +Consequently, a nonzero-demand row with no P call must receive at least two +ADDs. Its source coefficient otherwise stays zero. For any other nonzero-demand +row, at least one P call or at least two incoming ADDs is needed. Its bill +is therefore at least a_i. A zero-demand row has the trivial bound zero. + +This is **not** a per-edge statement for q >= 3. For example, the chronological +word + + E_01(1), E_12(1), E_01(-1), E_12(-1), E_02(1) + +is the identity on dirt over Z/4. Edge 2 -> 0 occurs once. The verifier checks +this control; the proof above counts three total arrivals at row 0 instead. + +### A necessary unit insertion and its extra price + +First suppose some r in U receives a P call. Row r costs at least mu_r and +all other rows cost at least a_i. The total is at least `A+mu_r-a_r=F_r`. + +Otherwise no row of U receives a P call. Some P coefficient must still be +a unit: if every inserted beta belonged to m, all source coefficients would +remain in m under additions and multiplication by arbitrary ring elements. +Their initial coefficients are zero, while the endpoint has a unit demand, +a contradiction. Choose a row r receiving a unit insertion; necessarily r is +in N. There are two possibilities: + +* Row r receives at least two P calls, so its bill is at least 2mu_r. +* It receives exactly one P call, with unit coefficient beta. With no incoming + ADD, its final source coefficient would equal beta, contradicting its + nonunit demand lambda_r (including lambda_r=0). Thus it receives at least + two ADDs, so its bill is at least `mu_r+2c_r`. + +Every unit-demand row has no insertion and costs at least 2c_i. Every other +row of N costs at least a_i. Adding these disjoint row bills gives T_r in +the first case and S_r in the second. This exhausts all words, including +repeated insertions, cancellations, feedback and arbitrary interleavings, +and proves the displayed minimum is a lower bound. + +## Constructions attaining every candidate + +All words below are chronological. For any nonzero-demand row besides the +chosen r, select direct insertion when mu_i <= 2c_i if that row is allowed +as a direct recipient below; otherwise select an echo. Zero-demand rows +besides r are untouched. Direct recipients receive `P_i(lambda_i)` and are +not used by any of the displayed row gates. + +**Unit root r: F_r.** Any other nonzero-demand row may be direct or echoed. +For each echoed i put `t_i=lambda_i lambda_r^(-1)`. Prepare all echoed rows +with `E_ir(-t_i)`, execute `P_r(lambda_r)`, then reverse the preparation with +negated coefficients. Each echoed row becomes + + (a_i-t_i a_r)+t_i(a_r+lambda_r p) = a_i+lambda_i p. + +Add the independent direct calls. The exact price is F_r. This is the +credited dirty-echo construction with a unit root. + +**Nonunit root r, repeated insertion: T_r.** Only other nonzero-demand rows +in N may be direct recipients; choose the cheaper direct/echo option for each. +All unit-demand rows are echoed. Prepare every echoed i with `E_ir(-lambda_i)`, +insert `P_r(1)`, undo preparation, then insert `P_r(lambda_r-1)`. The last +coefficient is nonzero since lambda_r is not a unit. Row r ends with its +own demand and every echoed row gets lambda_i p. Together with the direct +calls, the price is exactly T_r. This extends #5045's repeated-insertion word. + +**Nonunit root r, one insertion with mixing: S_r.** Choose any unit-demand +row j, and use the same direct/echo choices on other rows of N. Set +`b=lambda_r lambda_j^(-1)`. For every echoed i other than j prepare +`E_ij(-lambda_i lambda_j^(-1))`. Then execute #5045's two-row word + + E_rj(1-b), E_jr(-1), P_r(lambda_j), E_jr(1), E_rj(b-1). + +Its source column becomes `lambda_j e_r`, then +`lambda_j(e_r+e_j)`, then `lambda_r e_r+lambda_j e_j`. +The two pre-gates are the inverse of the two post-gates on dirt. Now undo +all earlier preparations in reverse order. Each echoed row uses the restored +unit-demand row j and ends correctly. Direct recipients are independent. + +Here b is a nonunit, so b != 1 and all four core ADDs are nonzero. Each +nonzero echoed coefficient is nonzero because lambda_j is a unit. The exact +price is S_r: two arrivals at r, two at every unit-demand row, and the chosen +minimum bill on other N rows. This also covers lambda_r=0. The original dirt +of this temporary recipient returns. Literal inversion of any complete word +reverses its gates and negates coefficients, with the same tariff. + +These constructions and the all-word lower bound prove the theorem. +Expanding it for q=3, lambda=(2,1,1) gives the eight-term table. More directly, +if a unit-demand row receives a source call, each of the six possible source +supports dominates its table vector. Otherwise only row 0 receives insertions: +two or more give T0, and a single unit insertion forces at least two arrivals +at all three rows, giving S0. Since every table vector is attained, they are +exactly the Pareto-minimal aggregate counts. The strict price witnesses above +show that no term can be removed from the positive-price envelope. + +## Why locality matters: an exact nonlocal counterexample + +Over Z/6 use demand `(2,3,1)`, mu=(10,10,100), c=(100,100,1). The two nonunit +source coefficients can combine to a unit, since `2*2+3=1 mod 6`. The word + + E_20(-2), E_21(-1), P_0(2), P_1(3), E_21(1), E_20(2) + +costs **24** and restores every dirt column. Applying the local-ring formula +outside its hypotheses would predict **32**. + +In fact 24 is optimal. A cheaper word cannot use a P at row 2 (price 100) +or an incoming ADD to row 0 or 1 (price 100). Thus each of rows 0,1 needs a +source call. Three such calls already cost 30, so a cheaper word must have +exactly one at each, with coefficients 2 and 3 respectively. To produce the +unit demand on row 2, both incoming edges must be used: either source alone +generates a proper ideal. Since rows 0,1 have unchanged dirt, each edge's +coefficients must separately sum to zero to restore row 2. Each used edge +therefore occurs at least twice. The bill is at least `10+10+4=24`. +This proves the counterexample without assuming a word-length bound. + +## Verification and scope + +The self-contained standard-library verifier checks the finite ring axioms, +locality, candidate prices, literal words and inverses on all formal input +columns. It includes prime-power residue rings and the non-chain local ring +`F2[e,h]/(e^2,eh,h^2)`. Zero-demand temporary recipients, all-unit boundaries, +all eight strict regimes, the five-ADD identity and the nonlocal example are +explicit controls. Wider row fixtures test the arbitrary-q construction. + +A separately implemented packed-state bidirectional Dijkstra oracle searches +unrestricted three-row Z/4 words. Its state retains all nine dirt coefficients +and all three source coefficients. Every nonzero coefficient and directed +ADD edge is permitted; there is no depth cutoff, forest restriction or +formula-based pruning. Search ends only when the two Dijkstra frontier +bounds certify the best meeting distance. Returned paths are replayed by +the primary literal interpreter and charged exactly. This is an implicit +finite-state shortest-path search, not enumeration of the entire state graph. + +The six local-ring fixtures cover 2,011 demand-list instances and 6,033 price +instances. All 25,179 candidate words pass 213,744 formal-column forward/inverse +executions; 6,688 additional literal forward/inverse executions cover the +eight three-row regimes and the Z/6 witness. Sixteen independent shortest-path +queries settle 154,814 entries in total (counting both directions and repeated +queries), alongside 15 explicit controls. Wider fixtures are deterministic +examples, not exhaustive arbitrary-row searches. + +Normal and optimized warning-strict commands are registered, with no external +scientific inputs or third-party dependencies. In disposable optimized-mode +copies, removing the extra unit-arrival charge, deleting a dirt-preparation +gate, or replacing the oracle's heterogeneous prices by unit weights each +causes an explicit rejection. Run the registered checks with: + +```sh +python3.12 -B scripts/research_package.py --package research/local-ring-row-fanout --check-only +python3.12 -B scripts/research_package.py --package research/local-ring-row-fanout +python3.12 -I -W error -B research/local-ring-row-fanout/verify.py +``` + +The all-ring-size, arbitrary-row and all-positive-price claims rest on the +written proof. Finite computations corroborate bounded cases. Independent +human review and proof-kernel acceptance are unclaimed. General directed-edge +prices, nonzero all-nonunit demand lists, nonlocal-ring tariffs and complete +physical caller costs remain open outside the stated cases. There is no new +supplier, precision/tape admission, selected-frontier change or κ. + +## Task, sources and overlap + +Scientific base: canonical main `a5df48c55ea806d7952b65acc9c76d878ff09b13`, +priority revision 7. [TASK.json](TASK.json) preserves the historical +`bit-helper-contract` card and marks this explicitly requested algebraic side +result as changed. [SOURCES.json](SOURCES.json) pins #4916's ring contract and +#5045's two-row proof/three-row handoff as historical provenance; no predecessor +executable is imported. #5139 motivates this next question but is not a proof +or runtime dependency. Its pending head is `ec44e8bec68b49a1ba7adaac8a0bba0192bd638c`. + +Entry overlap pagination covered 312 open PRs at 11:04 UTC and 4,318 Discussion +records at 11:06 UTC on 2026-10-23. All-state targeted three-row/nonunit/fanout +searches and live #5030/#1166 reads found no resolving successor in that +coverage. Sparse historical notes, arbitrary diffs and unpublished work were +not exhaustively searched. Submission refresh is recorded in the PR. + +## Open next questions + +1. **Independently priced directed edges for (2,1,1) over Z/4.** This is the + remaining part of the original three-row question. Start with one price + matrix where the cheap edges form a cycle, then compare a restoring word + against subset cuts plus the necessary unit-arrival charge. Counting only + total arrivals at each row loses which sources supplied them. +2. **All-nonunit local-ring demands.** Start with `(2,2,2)` over Z/4, then + `(e,h,e+h)` over the eight-element square-zero local ring. This tests shared + source injection without a unit demand. The necessary unit insertion used + here is absent, so this lower bound does not classify those cases. +3. **A physical caller.** Supply its complete stationary tariffs, including + source access, coefficient preparation, routing, precision and restoration, + and compare the full completed bill. That cost contract is missing here. + +## Credit + +Prepared by lee-phys with substantial OpenAI Codex assistance in derivation, +implementation, checking and writing. Apache-2.0. Credit Krzysztof Wójt #5045 +for the nonunit two-row theorem, repeated/mixing words and three-row question; +Nick Petalas #4916 for the ring-valued contract and free-module cut reasoning; +Ross Richardson #3063/#3121 for destination/edge tariffs and dirt restoration; +Cinna Davis #1944/#1968, Anthony #774, Oscar Fennell #759, Tekalign #3130, and +the retained lineage. #5139 records the continued three-row question. +The local-ring ideal fact is classical. The new contribution is the unit-arrival +price bound, its matching arbitrary-row constructors, the exact eight-term +three-row frontier and the explicit nonlocal boundary. diff --git a/research/local-ring-row-fanout/SOURCES.json b/research/local-ring-row-fanout/SOURCES.json new file mode 100644 index 0000000000..6dcf72a904 --- /dev/null +++ b/research/local-ring-row-fanout/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "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/unit-ring-dirty-fanout/README.md", + "usage": "provenance", + "git_blob": "70ce8559a0d35a5e2e9c47f0885c8042b22bb0ef", + "sha256": "70764fb3def04ba1b0a51e95cb023358fdaed5100d2440feecbaab0e85a9a5fe" + }, + { + "path": "research/two-row-nonunit-fanout/PROOF.md", + "usage": "provenance", + "git_blob": "1bd3b47624db83c45ca08fb498f2a84d814306c1", + "sha256": "d177967c73bd5e755c5f70964d5542420e23e36cad81c57452a222e50e356f77" + }, + { + "path": "research/two-row-nonunit-fanout/README.md", + "usage": "provenance", + "git_blob": "ea27d3919102a2e66ab4d3ed9170edafee633a06", + "sha256": "8aba08fc4a0c049ffaa20f12ca96bbfc582f853ed063a2f694a6bf853c637313" + } + ] +} diff --git a/research/local-ring-row-fanout/TASK.json b/research/local-ring-row-fanout/TASK.json new file mode 100644 index 0000000000..5a1120dc67 --- /dev/null +++ b/research/local-ring-row-fanout/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "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": "Exact arbitrary-positive destination-priced nonunit dirty-fanout tariff: three-row Z/4 demand (2,1,1), with a local-ring arbitrary-row extension, attaining words and all-interleaving lower bound.", + "scope_change_reason": "Explicit donor continuation of the three-dirty-row question in #5045/#5139. Refine to destination-dependent ADD prices c_ij=c_i, first solving (2,1,1) over Z/4, then any row count over commutative local rings with at least one unit demand. General directed-edge tariffs remain open.", + "bottleneck_link": "A structural source-sharing tariff and restoration result; it does not supply a physical caller or alter the selected multiplication exponent.", + "budget_minutes": 60, + "stop_rule": "Prove an exact tariff for the stated price family or produce a counterexample. Bound independent oracle searches to three-row Z/4 fixtures; retain arbitrary directed-edge prices and all-nonunit demands as explicit remaining questions.", + "outcome": "completed", + "evidence": "Written arbitrary-row local-ring proof and matching constructions; exact eight-vector Pareto frontier for Z/4 demand (2,1,1); exact Z/6 nonlocal counterexample 24 versus invalid extension 32. Standard-library verifier: 2,011 demand fixtures, 6,033 price instances, 25,179 candidate words, 213,744 formal-column forward/inverse executions, 6,688 literal forward/inverse executions, 16 independent packed-state bidirectional Dijkstra searches, 154,814 settled entries, 15 controls. Finite checks corroborate the proof; no proof-kernel or independent human acceptance is claimed.", + "author": "lee-phys, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, checking and writing. No sub-agents or independent reviewers.", + "open_questions": [ + { + "question": "Determine the tariff for independently priced directed ADD edges for (2,1,1) over Z/4.", + "why_it_matters": "This is the remaining part of the original three-row question.", + "first_step": "Try a directed cheap-edge cycle and compare restoring words with subset cuts and the necessary unit-arrival charge.", + "blocked_by": "Aggregate destination bills discard which incoming sources were used." + }, + { + "question": "Determine exact tariffs for nonzero all-nonunit demand lists over local rings.", + "why_it_matters": "Unit-demand rows are necessary for the lower bound proved here.", + "first_step": "Study (2,2,2) over Z/4 and (e,h,e+h) over the eight-element square-zero local ring.", + "blocked_by": "Without a unit target, a unit insertion is no longer necessary." + }, + { + "question": "Provide a physical caller realizing these complete gate tariffs.", + "why_it_matters": "The algebraic sharing theorem alone does not improve a multiplication exponent.", + "first_step": "Specify source access, coefficient preparation, routing, precision and restoration costs, then compare complete bills.", + "blocked_by": "No complete physical caller contract is provided." + } + ] +} diff --git a/research/local-ring-row-fanout/VERIFY.json b/research/local-ring-row-fanout/VERIFY.json new file mode 100644 index 0000000000..7c8b2d5bb3 --- /dev/null +++ b/research/local-ring-row-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": 120, + "checks": "Normal exact local-ring constructors, eight strict price regimes, 16 unrestricted three-row shortest paths, dirty restoration/inverses, zero-row controls and exact nonlocal boundary; no new kappa." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized exact local-ring constructors, eight strict price regimes, 16 unrestricted three-row shortest paths, dirty restoration/inverses, zero-row controls and exact nonlocal boundary; no new kappa." + } + ] +} diff --git a/research/local-ring-row-fanout/verify.py b/research/local-ring-row-fanout/verify.py new file mode 100644 index 0000000000..662106ef05 --- /dev/null +++ b/research/local-ring-row-fanout/verify.py @@ -0,0 +1,369 @@ +#!/usr/bin/env python3 +"""Exact finite checks for the scoped local-ring theorem in README.md. + +lee-phys with substantial OpenAI Codex assistance; Apache-2.0. +#3063/#4916/#5045 retain the credited return and echo/mixing constructions. +""" +from dataclasses import dataclass +from fractions import Fraction +from heapq import heappop, heappush +from itertools import product +from math import lcm +import json + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +@dataclass(frozen=True) +class Ring: + name: str + n: 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 sub(self, x, y): + return self.add[x][self.neg(y)] + + def inv(self, x): + return next(y for y in range(self.n) if self.mul[x][y] == 1) + + def units(self): + return frozenset(x for x in range(self.n) if 1 in self.mul[x]) + + def local(self): + nonunits = set(range(self.n))-self.units() + return (all(self.add[x][y] in nonunits for x in nonunits for y in nonunits) + and all(self.mul[x][y] in nonunits for x in nonunits for y in range(self.n))) + + +def residue(n): + return Ring(f'Z/{n}', n, tuple(tuple((x+y) % n for y in range(n)) for x in range(n)), + tuple(tuple(x*y % n for y in range(n)) for x in range(n))) + + +def square_zero_eight(): + def mul(x, y): + return ((x & 1)*(y & 1)) ^ ((x & 1)*(y & 6)) ^ ((y & 1)*(x & 6)) + return Ring('F2[e,h]/(e^2,eh,h^2)', 8, + tuple(tuple(x ^ y for y in range(8)) for x in range(8)), + tuple(tuple(mul(x, y) for y in range(8)) for x in range(8))) + + +def check_ring(r): + es, add, mul = range(r.n), r.add, r.mul + for x, y in product(es, repeat=2): + require(add[x][y] in es and mul[x][y] in es, 'ring closure') + require(add[x][y] == add[y][x] and mul[x][y] == mul[y][x], 'commutativity') + for x in es: + require(add[x][0] == x and mul[x][1] == x and mul[x][0] == 0, 'identities') + require(add[x][r.neg(x)] == 0, 'additive inverse') + for x, y, z in product(es, repeat=3): + require(add[add[x][y]][z] == add[x][add[y][z]], 'addition associativity') + require(mul[mul[x][y]][z] == mul[x][mul[y][z]], 'multiplication associativity') + require(mul[x][add[y][z]] == add[mul[x][y]][mul[x][z]], 'distributivity') + + +def raw_candidates(r, demand, mu, c): + """Algebraic expressions only; callers must establish the theorem domain.""" + units = r.units() + u = [i for i, x in enumerate(demand) if x in units] + n = [i for i, x in enumerate(demand) if x not in units] + a = [min(mu[i], 2*c[i]) if x != 0 else 0 for i, x in enumerate(demand)] + total = sum(a) + b = 2*sum(c[i] for i in u)+sum(a[i] for i in n) + out = [('F', i, total+mu[i]-a[i]) for i in u] + out += [('T', i, b+2*mu[i]-a[i]) for i in n] + out += [('S', i, b+mu[i]+2*c[i]-a[i]) for i in n] + return out + + +def candidates(r, demand, mu, c): + q = len(demand) + if q < 1 or len(mu) != q or len(c) != q or min((*mu, *c)) <= 0: + raise ValueError('positive prices and matching nonempty row arrays required') + if not all(isinstance(x, int) and 0 <= x < r.n for x in demand): + raise ValueError('demand outside the finite ring') + if not any(demand): + return [('Z', -1, 0)] + if not r.local(): + raise ValueError('the tariff theorem requires a local ring') + if not any(x in r.units() for x in demand): + raise ValueError('nonzero all-nonunit demands are outside the theorem') + return raw_candidates(r, demand, mu, c) + + +def reverse_word(r, word): + return [(i, j, r.neg(a)) for i, j, a in reversed(word)] + + +def construct(r, demand, mu, c, mode, root): + q = len(demand) + if mode == 'Z': + return [] + units = r.units() + direct = {root} + for i, x in enumerate(demand): + allowed = mode == 'F' or x not in units + if i != root and x != 0 and allowed and mu[i] <= 2*c[i]: + direct.add(i) + echoed = [i for i, x in enumerate(demand) if x != 0 and i not in direct] + other_calls = [(i, q, demand[i]) for i in sorted(direct-{root})] + if mode == 'F': + factor = r.inv(demand[root]) + pre = [(i, root, r.neg(r.mul[demand[i]][factor])) for i in echoed] + word = pre+[(root, q, demand[root])]+reverse_word(r, pre) + elif mode == 'T': + pre = [(i, root, r.neg(demand[i])) for i in echoed] + word = pre+[(root, q, 1)]+reverse_word(r, pre)+[(root, q, r.sub(demand[root], 1))] + elif mode == 'S': + pivot = next(i for i, x in enumerate(demand) if x in units) + factor = r.inv(demand[pivot]) + b = r.mul[demand[root]][factor] + pre = [(i, pivot, r.neg(r.mul[demand[i]][factor])) for i in echoed if i != pivot] + core = [(root, pivot, r.sub(1, b)), (pivot, root, r.neg(1)), + (root, q, demand[pivot]), (pivot, root, 1), (root, pivot, r.sub(b, 1))] + word = pre+core+reverse_word(r, pre) + else: + raise ValueError('unknown construction') + return word+other_calls + + +def execute(r, word, values): + out = list(values) + for i, j, a in word: + out[i] = r.add[out[i]][r.mul[a][out[j]]] + return tuple(out) + + +def endpoint(r, demand, word): + q = len(demand) + for k in range(q+1): + entry = tuple(int(j == k) for j in range(q+1)) + target = tuple(r.add[entry[i]][r.mul[demand[i]][entry[q]]] for i in range(q))+(entry[q],) + if execute(r, word, entry) != target or execute(r, reverse_word(r, word), target) != entry: + return False + return True + + +def bill(word, q, mu, c): + return sum(mu[i] if j == q else c[i] for i, j, _ in word) + + +def gate_counts(word, q): + return tuple(sum(i == k and j == q for i, j, _ in word) for k in range(q)) + tuple( + sum(i == k and j != q for i, j, _ in word) for k in range(q)) + + +# The oracle below uses only modular packed affine states and primitive gates. +# It never calls the formula, local-ring criterion or word constructors. +def packed_tables(): + return [None]+[bytes(sum(((((x >> (2*k)) & 3)+a*((y >> (2*k)) & 3)) % 4) << (2*k) + for k in range(4)) for x in range(256) for y in range(256)) + for a in (1, 2, 3)] + + +def packed_neighbors(state, weights, tables): + for i in range(3): + shift = 8*i + row = (state >> shift) & 255 + source = row >> 6 + for a in (1, 2, 3): + updated = (row & 63) | (((source+a) & 3) << 6) + yield state ^ ((row ^ updated) << shift), weights[i], (i, 3, a) + for j in range(3): + if i == j: + continue + other = (state >> (8*j)) & 255 + index = (row << 8) | other + for a in (1, 2, 3): + updated = tables[a][index] + yield state ^ ((row ^ updated) << shift), weights[3+i], (i, j, a) + + +def oracle(demand, mu, c, tables): + scale = lcm(*(Fraction(x).denominator for x in (*mu, *c))) + weights = tuple(int(Fraction(x)*scale) for x in (*mu, *c)) + require(min(weights) > 0, 'oracle positive prices') + start = 1 | (4 << 8) | (16 << 16) + goal = start | sum(x << (8*i+6) for i, x in enumerate(demand)) + if start == goal: + return Fraction(0), [], (0, 0) + dist = [{start: 0}, {goal: 0}] + parents = [{start: None}, {goal: None}] + queues = [[(0, start)], [(0, goal)]] + best, meeting = None, None + settled = [0, 0] + while queues[0] and queues[1]: + for side in (0, 1): + while queues[side] and queues[side][0][0] != dist[side][queues[side][0][1]]: + heappop(queues[side]) + if not queues[0] or not queues[1]: + break + if best is not None and queues[0][0][0]+queues[1][0][0] >= best: + break + side = int(queues[1][0][0] < queues[0][0][0]) + du, u = heappop(queues[side]) + settled[side] += 1 + other_dist = dist[1-side] + for v, cost, gate in packed_neighbors(u, weights, tables): + dv = du+cost + if v not in dist[side] or dv < dist[side][v]: + dist[side][v] = dv + parents[side][v] = (u, gate) + heappush(queues[side], (dv, v)) + if v in other_dist: + total = dv+other_dist[v] + if best is None or total < best: + best, meeting = total, v + require(meeting is not None, 'oracle failed to connect endpoints') + forward, back = [], [] + u = meeting + while parents[0][u] is not None: + u, gate = parents[0][u] + forward.append(gate) + u = meeting + while parents[1][u] is not None: + u, (i, j, a) = parents[1][u] + back.append((i, j, (-a) % 4)) + path = list(reversed(forward))+back + return Fraction(best, scale), path, tuple(settled) + + +def price_fixtures(q): + return [((1,)*q, (1,)*q), + (tuple(2*i+5 for i in range(q)), tuple(i+1 for i in range(q))), + (tuple(Fraction(i+1, 3) for i in range(q)), tuple(Fraction(q-i, 5) for i in range(q)))] + + +def main(): + rings = [residue(n) for n in (2, 3, 4, 8, 9)]+[square_zero_eight()] + totals = dict(demands=0, price_instances=0, words=0, basis_forward_inverse=0, + literal_forward_inverse=0, oracle_runs=0, oracle_settled=0, controls=0) + fixture_records = [] + def check_problem(r, demand): + totals['demands'] += 1 + for mu, c in price_fixtures(len(demand)): + options = candidates(r, demand, mu, c) + totals['price_instances'] += 1 + for mode, root, expected in options: + word = construct(r, demand, mu, c, mode, root) + require(all(a != 0 for _, _, a in word), 'zero gate in exact-price construction') + require(endpoint(r, demand, word), f'word endpoint/inverse: {r.name} {demand} {mode}{root}') + require(bill(word, len(demand), mu, c) == expected, 'exact candidate price') + totals['words'] += 1 + totals['basis_forward_inverse'] += 2*(len(demand)+1) + for r in rings: + check_ring(r) + require(r.local(), 'positive local-ring fixture') + count = 0 + units = r.units() + for q in (1, 2, 3): + for demand in product(range(r.n), repeat=q): + if not any(demand) or any(x in units for x in demand): + check_problem(r, demand) + count += 1 + for q in (4, 5, 7): + nonunit = next((x for x in range(1, r.n) if x not in units), 0) + for offset in range(q): + demand = tuple((1, nonunit, 0)[(i+offset) % 3] for i in range(q)) + check_problem(r, demand) + count += 1 + fixture_records.append({'ring': r.name, 'demand_lists': count}) + + four = residue(4) + demand = (2, 1, 1) + names = ('D', 'F01', 'F02', 'F12', 'F1', 'F2', 'T0', 'S0') + vectors = ((1,1,1,0,0,0), (1,1,0,0,0,2), (1,0,1,0,2,0), (0,1,1,2,0,0), + (0,1,0,2,0,2), (0,0,1,2,2,0), (2,0,0,0,2,2), (1,0,0,2,2,2)) + regimes = ((1,1,1,1,1,1), (1,1,20,10,10,1), (1,20,1,10,1,10), (20,1,1,1,10,10), + (20,1,20,1,10,1), (20,20,1,1,1,10), (1,20,20,10,1,1), (5,20,20,1,1,1)) + chosen_words = [] + for index, prices in enumerate(regimes): + costs = [sum(x*y for x, y in zip(v, prices)) for v in vectors] + require(costs[index] < min(v for i, v in enumerate(costs) if i != index), 'strict eight-term regime') + totals['controls'] += 1 + mu, c = prices[:3], prices[3:] + mode, root, value = min(candidates(four, demand, mu, c), key=lambda x: x[2]) + word = construct(four, demand, mu, c, mode, root) + require(value == costs[index] and gate_counts(word, 3) == vectors[index], 'three-row table count') + chosen_words.append(word) + for entry in product(range(4), repeat=4): + target = tuple((entry[i]+demand[i]*entry[3]) % 4 for i in range(3))+(entry[3],) + require(execute(four, word, entry) == target, 'literal three-row word') + require(execute(four, reverse_word(four, word), target) == entry, 'literal inverse') + totals['literal_forward_inverse'] += 2 + + # Three-row identity with one occurrence of a particular directed edge. + relator = [(0,1,1), (1,2,1), (0,1,3), (1,2,3), (0,2,1)] + require(endpoint(four, (0,0,0), relator), 'five-ADD identity') + require(sum((i, j) == (0, 2) for i, j, _ in relator) == 1, 'single edge-occurrence control') + totals['controls'] += 1 + # Source column alone would miss this failed restoration. + bad = chosen_words[6][1:] + require(execute(four, bad, (0,0,0,1)) == (2,1,1,1), 'dirty-only mutation premise') + require(not endpoint(four, demand, bad), 'reject missing dirt preparation') + totals['controls'] += 1 + try: + candidates(four, (2,2,2), (1,1,1), (1,1,1)) + except ValueError: + totals['controls'] += 1 + else: + raise RuntimeError('accepted all-nonunit demand outside the theorem') + + six = residue(6) + check_ring(six) + nonlocal_demand, mu, c = (2,3,1), (10,10,100), (100,100,1) + require(not six.local(), 'nonlocal fixture') + try: + candidates(six, nonlocal_demand, mu, c) + except ValueError: + totals['controls'] += 1 + else: + raise RuntimeError('accepted nonlocal ring') + require(min(x[2] for x in raw_candidates(six, nonlocal_demand, mu, c)) == 32, 'invalid extension discriminator') + witness_word = [(2,0,4), (2,1,5), (0,3,2), (1,3,3), (2,1,1), (2,0,2)] + require(bill(witness_word, 3, mu, c) == 24 and endpoint(six, nonlocal_demand, witness_word), 'nonlocal cost-24 word') + for entry in product(range(6), repeat=4): + target = tuple((entry[i]+nonlocal_demand[i]*entry[3]) % 6 for i in range(3))+(entry[3],) + require(execute(six, witness_word, entry) == target and execute(six, reverse_word(six, witness_word), target) == entry, + 'literal nonlocal counterexample') + totals['literal_forward_inverse'] += 2 + totals['controls'] += 1 + + tables = packed_tables() + oracle_cases = [(name, demand, p[:3], p[3:]) for name, p in zip(names, regimes)] + oracle_cases += [ + ('requested-first-matrix', demand, (1,9,9), (1,1,1)), + ('expensive-source-mixing', demand, (100,1000,1000), (1,1,1)), + ('repeat-mix-tie', demand, (2,9,9), (1,1,1)), + ('rational', demand, (Fraction(3,2),Fraction(7,2),Fraction(11,2)), + (Fraction(1,3),Fraction(2,3),Fraction(4,3))), + ('zero-temporary-recipient', (0,1,2), (1,9,9), (1,1,1)), + ('permuted-nonunit-1', (1,2,3), (9,1,9), (1,1,1)), + ('permuted-nonunit-2', (1,3,2), (9,9,1), (1,1,1)), + ('unit-demand-calibration', (1,3,1), (1,9,9), (1,1,1)), + ] + oracle_records = [] + for name, target, mu, c in oracle_cases: + value, path, settled = oracle(target, mu, c, tables) + predicted = min(x[2] for x in candidates(four, target, mu, c)) + require(value == predicted, f'oracle mismatch: {name}: {value} != {predicted}') + require(endpoint(four, target, path) and bill(path, 3, mu, c) == value, 'oracle path replay and bill') + totals['oracle_runs'] += 1 + totals['oracle_settled'] += sum(settled) + oracle_records.append({'case': name, 'optimum': str(value), 'settled': list(settled)}) + print('CHECK_ORACLE', name, str(value), flush=True) + require(oracle_records[8]['optimum'] == '6' and oracle_records[9]['optimum'] == '106', 'named exact optima') + totals['controls'] += 2 + print(json.dumps({'fixtures': fixture_records, 'counts': totals, 'oracle': oracle_records}, sort_keys=True)) + print('PASS_LOCAL_RING_ROW_FANOUT no_new_kappa') + + +if __name__ == '__main__': + main()