From 4e08457f4d0b69c00a6ca62eca81c8d0a55f3e60 Mon Sep 17 00:00:00 2001 From: lizhi Date: Fri, 30 Oct 2026 01:56:43 +0800 Subject: [PATCH] Prove exact tariffs for independent radical fanout triples --- research/r16-radical-triple-fanout/README.md | 368 +++++++++++++++++ .../r16-radical-triple-fanout/SOURCES.json | 42 ++ research/r16-radical-triple-fanout/TASK.json | 83 ++++ .../r16-radical-triple-fanout/VERIFY.json | 34 ++ research/r16-radical-triple-fanout/verify.py | 380 ++++++++++++++++++ 5 files changed, 907 insertions(+) create mode 100644 research/r16-radical-triple-fanout/README.md create mode 100644 research/r16-radical-triple-fanout/SOURCES.json create mode 100644 research/r16-radical-triple-fanout/TASK.json create mode 100644 research/r16-radical-triple-fanout/VERIFY.json create mode 100644 research/r16-radical-triple-fanout/verify.py diff --git a/research/r16-radical-triple-fanout/README.md b/research/r16-radical-triple-fanout/README.md new file mode 100644 index 0000000000..a122a5de58 --- /dev/null +++ b/research/r16-radical-triple-fanout/README.md @@ -0,0 +1,368 @@ +# Exact tariff for three independent radical demands + +**Scoped written proof with exact finite corroboration; no new kappa.** +For three arbitrary dirty rows over the sixteen-element ring + + R16 = F2[e,h,z]/(e,h,z)^2, + lambda = (e,h,e+h+z), + +this package determines the exact cost for every six strictly positive +receiving-row prices. The price envelope has **ten indispensable linear +terms**, with matching words and a lower bound covering every finite +interleaving. The theorem extends to every commutative unital local ring +whose three demand classes in `m/m^2` are linearly independent over `R/m`. +Neither finiteness nor `m^2=0` is needed for that extension. + +This answers the non-zero-sum, three-generator question explicitly left in +lee-phys [#5259](https://github.com/CrocSwap/integer-mult-bounds/pull/5259). +That predecessor's nineteen-term theorem concerns nonprincipal **zero-sum** +triples. Here the sum is z, and its cheaper two-insertion families do not +supply the requested endpoint. Ali Romman's +[#5310](https://github.com/CrocSwap/integer-mult-bounds/pull/5310) +classifies source-insertion feasibility; it does not settle this total tariff. + +## Contract and theorem + +Let R be a commutative local ring with `1 != 0`, maximal ideal m and residue +field `k=R/m`. Assume + + lambda_i in m, i=0,1,2, + [lambda_0], [lambda_1], [lambda_2] are k-linearly independent in m/m^2. + +There are exactly three independent arbitrary dirty rows `a_i in R^w`, +`w >= 1`, and one disjoint preserved source `p in R^w`. A fixed finite +straight-line word must send each row to `a_i+lambda_i p` for every input. +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; ADD prices +depend only on the receiving row. Zero-coefficient gates may be deleted. +There are no auxiliary rows, clearing operations, observations, adaptive +branches or free basis changes. An inverse execution has its own bill. + +**Theorem.** For distinct i,j,k define + + D = mu_0 + mu_1 + mu_2, + T_i = 2mu_i + 2c_j + 2c_k, + R_ij;k = 2mu_i + mu_j + 2c_k. + +Then the exact optimum is the minimum of D, the three T terms and the six R +terms. Equivalently, writing `{i,j}={0,1,2}\{k}`, + + B_k = mu_i + mu_j + min(mu_i,mu_j) + 2c_k, + OPT = min(D,T_0,T_1,T_2,B_0,B_1,B_2). + +Each of the ten expanded terms is uniquely cheapest for some strictly +positive prices. This is a complete **price envelope**, not a claim that +these ten count vectors form the complete componentwise Pareto frontier. +The distinction matters in the two-root, two-insertion case below. + +For R16, `m=(e,h,z)`, `m^2=0`, and `k=F2`. The coefficient matrix of +`(e,h,e+h+z)` in the basis `(e,h,z)` is triangular with diagonal entries 1, +so the hypothesis holds. With common prices `mu_i=mu` and `c_i=c`, + + OPT = min(3mu, 2mu+4c). + +The switch is at `mu=4c`. With unequal prices `(mu;c)=(3,5,10;1,3,2)`, +the optimum is **15**, attained by `R_01;2`. With `(1,9,9;1,1,1)`, it is +**6**, attained by `T_0`. + +## Lower bound for arbitrary interleavings + +Track the three dirt coefficients and the source coefficient in each row. +The dirt matrix starts at I. Every ADD is an invertible elementary row +operation, and an insertion does not affect dirt. Thus every prefix and +suffix dirt matrix is invertible. Correctness on all inputs forces the +final dirt matrix to be I and the final source column to be lambda. Scalar +inputs already force these identities; they also suffice for every width w. + +### Incoming-row return lemma + +A row cannot receive exactly one nonzero ADD in a restoring word. Suppose +its only incoming ADD is `E_ij(alpha)`, and let M be the preceding invertible +dirt matrix. Row i has remained the standard row e_i. The update changes it +to `e_i+alpha m_j`, where m_j is row j of M. No subsequent operation changes +this dirt row. Restoration would imply `alpha m_j=0`; right multiplication +by `M^-1` gives `alpha e_j=0`, hence `alpha=0`, a contradiction. + +Consequently, a row with a nonzero demand and no insertion must receive at +least two ADDs. With no incoming ADD its source coefficient would stay zero; +exactly one is excluded by the lemma. This is the incoming-row argument +credited to #3063/#4916/#5163 and used in #5259. It applies to the **total** +number of incoming ADDs, not separately to each directed edge. + +### Two insertions must both use units + +If the insertion coefficients are beta_t and their rows are r_t, linearity +of the source column gives the exact identity + + lambda = sum_t (L_t e_(r_t)) beta_t, (1) + +where L_t is the invertible matrix of all ADDs after insertion t. Later +insertions add their own terms and do not change this propagation rule. +Equation (1) permits arbitrary earlier/later insertions, cancellations and +feedback through other rows. + +Every element of a local ring is either in m or is a unit. There is no +zero-insertion solution because all three demands are nonzero. + +* With one insertion having a unit coefficient, reduction of (1) modulo m + gives a nonzero field scalar times a column of an invertible matrix. That + column cannot vanish, whereas lambda reduces to zero. If instead the + coefficient lies in m, reducing (1) modulo `m^2` places all three demand + classes in the span of one class. Both possibilities contradict the + hypotheses. Thus at least two insertions are necessary. +* With exactly two insertions and exactly one unit coefficient, the same + reduction modulo m leaves one nonzero invertible-matrix column and gives + a contradiction. If neither coefficient is a unit, both lie in m. For + `beta in m`, the class of `a beta` in `m/m^2` equals the residue of a times + the class of beta. Therefore (1) puts the three demand classes in the span + of the two insertion classes, which has dimension at most two. This also + contradicts independence. + +Hence **every solution with exactly two insertions has two unit insertion +coefficients**. This conclusion does not rule out such words: the matching +T words below use two units. It rules out the rank-two nonunit mechanism. + +### Classify the insertion support + +Write S for the set of rows receiving nonzero insertions, and K_i for the +number of nonzero incoming ADDs into row i. + +1. If S contains all three rows, the bill is at least D. +2. If `S={i}`, the preceding argument forces at least two insertions into i. + The other two rows have nonzero demand and no insertion, so `K_j,K_k>=2`. + The bill is at least T_i. +3. Let `S={i,j}` and let k have no insertion, so `K_k>=2`. If row i receives + at least two insertions, the bill is at least `R_ij;k`; the same conclusion + with i,j interchanged holds if j receives at least two. +4. The only remaining case has exactly one insertion in each of i and j. + Both insertion coefficients are units. If i received no ADD, its final + source coefficient would equal its sole unit insertion coefficient, + contrary to `lambda_i in m`. Thus `K_i>0`, hence `K_i>=2` by the return + lemma; likewise `K_j>=2`. Every such word costs at least + + mu_i+mu_j+2c_i+2c_j+2c_k + = (T_i+T_j)/2 + c_i+c_j + > min(T_i,T_j). (2) + + It therefore cannot be cheapest at any strictly positive price vector. + +These alternatives exhaust all finite words and prove the stated lower +bound. In particular, (2) is a **price-dependent comparison with a pair of +other words**, not componentwise domination by a single count vector. It +establishes the envelope without classifying all unexposed Pareto vectors. + +## Matching words + +All words below are listed in chronological order. For any current dirty +rows, the echo + + E_ji(a), P_i(b), E_ji(-a) + +increments root i by `b p` and receiver j by `-ab p`, while restoring all +original dirt. Indeed j first becomes `A_j+a A_i`, root i then becomes +`A_i+b p`, and the last gate leaves `A_j-ab p`. This calculation remains +valid when A_i and A_j already contain source contributions. + +Set `u_i=lambda_i-1`. Since `lambda_i in m`, u_i is a unit. Independence +makes every lambda_i nonzero. Thus all coefficients in these words are +nonzero and their displayed count vectors are exact. + +* **D:** `P_0(lambda_0), P_1(lambda_1), P_2(lambda_2)`. +* **T_i:** for the other two rows j,k, use + + E_ji(-lambda_j), P_i(1), E_ji(lambda_j), + E_ki(-lambda_k u_i^-1), P_i(u_i), E_ki(lambda_k u_i^-1). + + The first echo delivers lambda_j to j, the second delivers lambda_k to k, + and i receives `1+u_i=lambda_i`. The bill is `2mu_i+2c_j+2c_k`. +* **R_ij;k:** use + + E_ki(-lambda_k), P_i(1), E_ki(lambda_k), + P_i(u_i), P_j(lambda_j). + + The echo delivers lambda_k to k; the last two insertions leave the + remaining demands. The bill is `2mu_i+mu_j+2c_k`. + +For R16, signs disappear, `u_i=1+lambda_i` is self-inverse and +`lambda_k u_i^-1=lambda_k`. In particular a six-gate T_0 word is + + E_10(h), P_0(1), E_10(h), + E_20(e+h+z), P_0(1+e), E_20(e+h+z). + +These constructions attain every term of the lower envelope. Combined with +the preceding exhaustive lower bound, they prove the theorem for arbitrary +strictly positive real prices, independently of finite computation. + +## All ten terms are necessary + +Prices below are ordered `(mu_0,mu_1,mu_2;c_0,c_1,c_2)`. + +| Unique minimum | Positive prices | Value | Next smallest term | +| --- | --- | ---: | ---: | +| D | `(1,1,1;1,1,1)` | 3 | 5 | +| T_0 | `(1,3,3;1,1,1)` | 6 | 7 | +| R_01;2 | `(1,2,5;1,2,1)` | 6 | 7 | + +Row permutations expose all three T and all six R terms. A uniquely +minimizing term remains so in a neighborhood of its witness prices, so it +cannot be omitted from the formula. The verifier checks all permutations. + +The rank hypothesis is substantive. For the lower-rank demand `(e,h,e+h)` +in the **same R16**, the predecessor M word + + E_01(1), E_20(1), P_0(e+h), P_1(h), E_20(1), E_01(1) + +is correct and costs **14** at `(3,5,10;1,3,2)`, less than the present +formula's **15**. Its classes are dependent; the theorem does not apply. +The current three-generator target cannot use this cheaper word. + +## Finite evidence and reproduction + +`verify.py` is self-contained standard-library Python. Source files are +historical provenance, not runtime inputs. The coordinate ring interpreter +checks all commutative ring axioms, identifies the unique maximal ideal and +its square, and enumerates **every** ordered demand triple satisfying the +independence hypothesis in these three rings: + +| Ring | Size | Size of m | Size of m^2 | Accepted triples | +| --- | ---: | ---: | ---: | ---: | +| `F2[e,h,z]/(e,h,z)^2` | 16 | 8 | 1 | 168 | +| `F3[e,h,z]/(e,h,z)^2` | 81 | 27 | 1 | 11,232 | +| `(Z/4)[x,y]/(x,y)^2` | 64 | 32 | 4 | 10,752 | + +The first two counts are `|GL_3(F2)|=7*6*4` and +`|GL_3(F3)|=26*24*18`. In the third ring, `m=(2,x,y)` and +`m^2={0,2x,2y,2x+2y}`; there are `168*4^3` independent triples. +This last fixture tests the extension beyond square-zero maximal ideals. + +The checks cover 22,152 demands, 221,520 words and 1,772,160 formal +forward/inverse column evaluations. For the requested R16 demand they also +check all `16^4=65,536` scalar dirty/source inputs for each of ten words in +both directions: 1,310,720 literal evaluations. Eleven controls exercise +rank loss, a unit demand, nonlocality, missing dirty preparation, an +odd-characteristic sign error, omission of a necessary unit inverse, +the false per-edge return lemma and nonpositive prices. + +An independent implementation packs the complete `3 x 4` coefficient +matrix into 48 bits and uses bit arithmetic for R16. All 1,048,576 packed +coefficient/row products are compared with the coordinate implementation. +Bidirectional Dijkstra then permits every nonzero coefficient for every +one of the three insertion and six ADD locations: **135 neighbors per +state**, with no restriction on intermediate dirt, source support, unit +coefficients or gate patterns. It has no formula-derived cutoff or initial +upper bound. It stops only when its queue lower bound meets the best +complete path. Guards at 50,000 settled states and 1,000,000 combined +discovered states (checked before each expansion) raise an error rather +than certifying an unfinished search. Every returned path is replayed in +the coordinate interpreter and its bill is recomputed. + +The four price queries use `(1,1,1;1,1,1)`, `(1,10,10;10,1,1)`, +`(1,2,10;10,10,1)` and `(1/2,2/3,3/4;1,4/3,5/4)`. Their exact optima are +respectively `3`, `6`, `6` and `23/12`, covering strict D, T and R regimes +and nonintegral prices. +These queries corroborate the proof; they are not an exhaustive price scan +or the justification for the all-ring/all-real-price theorem. An exploratory +search at `(1/2,4/3,7/3;2/3,3/4,1/5)` was interrupted before certification; +another at `(1/2,1,5/2;1/2,1,2/3)` hit a resource guard. Neither is counted +as evidence. The registered cases use bounded representative prices. + +From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/r16-radical-triple-fanout --check-only +python3.12 -B scripts/research_package.py --package research/r16-radical-triple-fanout +``` + +`VERIFY.json` registers isolated, warning-strict normal and optimized +Python 3.12 executions. Direct exported-source replay is also supported: + +```sh +python3.12 -I -W error -B research/r16-radical-triple-fanout/verify.py +python3.12 -I -O -W error -B research/r16-radical-triple-fanout/verify.py +``` + +The script reports `PASS_R16_RADICAL_TRIPLE_FANOUT no_new_kappa` on success. +Checks use explicit exceptions, so `-O` does not disable them. + +Local validation used CPython 3.12.13 on macOS 26.7.1 (x86_64). Both +registered commands and metadata/source pins pass; one direct normal replay +took 11.83 seconds, a single-run observation rather than a benchmark. The +four search queries settled 8,465 entries in total. Three disposable +optimized-script mutations were rejected: charging a T word for only one +insertion, deleting its first dirty preparation, and replacing the required +unit inverse by 1. These checks do not require an installed solver or network. + +## Provenance, overlap and limits + +Base: canonical main `a5bff3bf133e482541c09eba4e773884bdb2b1b7`, refreshed at +entry on 2026-10-29 UTC. Exact Git-blob and SHA256 pins are in `SOURCES.json`. +`TASK.json` retains priority revision 8 and the original `bit-helper-contract` +card, explicitly recording the donor-assigned algebraic scope change. +No random card was drawn or rerolled. + +The immediately preceding overlap snapshot completely paginated 328 open +PRs at 17:27 UTC and 5,940 Discussion/comment/reply records at 17:30 UTC. +Entry checks refreshed main, current coordination threads and all-state PR +searches for the nonprincipal/three-generator and e,h,z fanout problem. +At the 17:54 UTC submission checkpoint, canonical main remained unchanged; +the refreshed discussions/handoffs/fanout thread and all-state PR searches +found no updates since the snapshot and no same-scope result or active claim. +The local +note scan covered 42 packages and omitted 8,581 tracked notes in the sparse +checkout; it was not treated as a complete repository-history review. +This is a bounded project-overlap check, not a proof of global novelty. + +The source pins all resolve at the base commit, which is the direct parent +of this contribution. The optional full-history preflight is not claimed: +this is a shallow checkout. Hosted CI and independent review are separate +pending steps; no selected-operator, Lean, Docker or historical suite replay +is needed for this isolated five-file addition. + +The written lower bound requires mathematical review. Finite replay is not +proof-kernel verification, independent human approval or admission as a +multiplication supplier. This package does not settle directed-edge tariffs, +nonlocal rings, dependent demand classes, extra helpers or all unexposed +Pareto vectors. Applying a word physically requires pricing coefficients, +source access, routing, precision, stock and the full H2/K interface. The +selected frontier is unchanged and no new kappa is claimed. + +## Open next questions + +The structured questions are also recorded in `TASK.json`. + +1. Determine the **complete Pareto frontier** for the requested R16 demand. + The exact positive-price envelope can omit unexposed vectors. The first + unresolved branch is one unit insertion in each of two different rows: + classify which restoring count vectors are attainable, beginning with + `(P_i,P_j,P_k)=(1,1,0)` and `K=(2,2,2)`. Equation (2) settles their price + relevance but neither their existence nor componentwise minimality. +2. Determine the tariff with independently priced directed ADD edges. + This matters when two parents feeding the same row have different costs. + Begin with a cheap directed three-cycle and full dirt tracking. The + present incoming-row lemma loses edge information; the five-ADD identity + in the verifier rules out simply imposing two calls on every used edge. + +These are proposed follow-ups, not overlap reservations or claims of novelty. + +## 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, count bookkeeping and bidirectional shortest-path method +adapt lee-phys #5259/#5514, pinned here; predecessors remain unchanged. +Credit Ali Romman #5266/#5310 for source-insertion feasibility, lee-phys +#5139/#5163/#5259 for ideal invariance, the local-ring boundary and the +non-zero-sum handoff, Nick Petalas #5208/#4916 for the equal-demand theorem +and ring-valued contract, Krzysztof Wojt #5045 for source-count classification +and two-row restoring words, 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 independent-class +obstruction to nonunit two-insertion words, the two-root price comparison, +and the matching ten-term envelope over general commutative local rings. diff --git a/research/r16-radical-triple-fanout/SOURCES.json b/research/r16-radical-triple-fanout/SOURCES.json new file mode 100644 index 0000000000..7fcfd80d4a --- /dev/null +++ b/research/r16-radical-triple-fanout/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/orthogonal-boolean-fanout/README.md", + "usage": "provenance", + "git_blob": "fa02e1e5850044a9aafb6131f6e50421e5c34d1b", + "sha256": "9ae4f5beb80fbb0795bd40c148eb4a22d7c7b1def2e9af61df855df57151b5d6" + }, + { + "path": "research/orthogonal-boolean-fanout/verify.py", + "usage": "provenance", + "git_blob": "e4ab0df938157a70ab2b06e327c4886f2b38c849", + "sha256": "3a18d270a17d51c8dded7698f9d8a0ca53a5e5ffa199b714e21614ceff1d88e2" + }, + { + "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" + } + ] +} diff --git a/research/r16-radical-triple-fanout/TASK.json b/research/r16-radical-triple-fanout/TASK.json new file mode 100644 index 0000000000..7ac65d4fba --- /dev/null +++ b/research/r16-radical-triple-fanout/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the exact arbitrary-positive receiving-row tariff for demand (e,h,e+h+z) over F2[e,h,z]/(e,h,z)^2, and prove its extension to three demand classes independent in m/m^2 over any commutative unital local ring.", + "scope_change_reason": "The donor explicitly assigned the three-generator non-zero-sum mathematical follow-up left by #5259. This is a scoped algebraic side result, not a replacement H2/K interface or an admitted supplier construction.", + "bottleneck_link": "Provides matching dirty-input words and an all-interleaving lower bound under complete abstract gate prices. Physical supplier admission still requires coefficient, source-access, routing, precision, stock and complete interface accounting. No selected-kappa improvement is claimed.", + "budget_minutes": 60, + "stop_rule": "Finish with a strict proof and matching constructions for every exposed price term, or record a precise obstruction within one approximately 60-minute session. Bound corroboration to three finite rings, four full-state price queries and targeted failure controls.", + "outcome": "completed", + "evidence": "README.md proves the exact ten-term positive-price envelope for independent radical triples over commutative local rings. Finite corroboration covers all 22,152 applicable triples in three rings, 221,520 words, 1,772,160 formal forward/inverse column evaluations, 1,310,720 literal evaluations, ten strict exposures, eleven controls and four independent full-state shortest paths. This is not a complete Pareto-frontier classification, proof-kernel verification, independent human review or physical supplier admission. Registered warning-strict normal/optimized CPython 3.12.13 replay and metadata/source-pin validation pass; three disposable optimized semantic mutations reject. The four oracle queries settle 8,465 entries.", + "author": "lee-phys, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in source inspection, mathematical derivation, construction, Python implementation, finite experiments, verification and writing. No subagents or independent reviewers were used.", + "open_questions": [ + { + "question": "What is the complete componentwise Pareto frontier for (e,h,e+h+z) over R16?", + "why_it_matters": "The exact positive-price envelope can omit unexposed attainable vectors, and the lower bound uses a price-dependent comparison with a pair of words.", + "first_step": "Classify attainable words with one unit insertion in each of two different rows, starting with insertion counts (1,1,0) and incoming ADD counts (2,2,2).", + "blocked_by": "The average-cost inequality excludes this branch from price optimality but does not decide its feasibility or componentwise minimality." + }, + { + "question": "What is the exact tariff for the same R16 demand with independent prices on all six directed ADD edges?", + "why_it_matters": "Two parents feeding the same row can have different physical prices, which destination totals do not distinguish.", + "first_step": "Probe a cheap directed three-cycle with full dirt tracking and retain edge counts in the source-support classification.", + "blocked_by": "The incoming-row return lemma cannot be strengthened to a per-edge lemma; the five-ADD identity is a counterexample." + } + ] +} diff --git a/research/r16-radical-triple-fanout/VERIFY.json b/research/r16-radical-triple-fanout/VERIFY.json new file mode 100644 index 0000000000..74ae90238f --- /dev/null +++ b/research/r16-radical-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 ring axioms, all independent radical triples in three finite rings, ten constructions and inverses, literal R16 dirty inputs, positive-price exposure, eleven hypothesis/sign/dirty-input controls and four unrestricted full-state shortest paths; no new kappa." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Optimized exact ring axioms, all independent radical triples in three finite rings, ten constructions and inverses, literal R16 dirty inputs, positive-price exposure, eleven hypothesis/sign/dirty-input controls and four unrestricted full-state shortest paths; no new kappa." + } + ] +} diff --git a/research/r16-radical-triple-fanout/verify.py b/research/r16-radical-triple-fanout/verify.py new file mode 100644 index 0000000000..5e5ebe9ce3 --- /dev/null +++ b/research/r16-radical-triple-fanout/verify.py @@ -0,0 +1,380 @@ +#!/usr/bin/env python3 +"""Bounded exact corroboration of README.md; no new kappa. + +lee-phys, with substantial OpenAI Codex assistance; Apache-2.0. +The ring interpreter and bidirectional search adapt the credited #5259/#5514 +verifiers. No predecessor package is imported or needed at runtime. +""" +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 self.add[x].index(0) + + def inv(self, x): + return self.mul[x].index(self.one) + + +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 truncated_polynomials(modulus, variables): + # Constant plus independent variables, with every variable product zero. + # Modulus 4 retains 2*x != 0 and a non-square-zero maximal ideal. + width = variables+1 + + def digits(x): + return tuple((x//modulus**k) % modulus for k in range(width)) + + def add(x, y): + a, b = digits(x), digits(y) + return sum(((a[k]+b[k]) % modulus)*modulus**k for k in range(width)) + + def mul(x, y): + a, b = digits(x), digits(y) + return (a[0]*b[0]) % modulus + sum( + ((a[0]*b[k]+a[k]*b[0]) % modulus)*modulus**k for k in range(1, width)) + + return ring_from_functions(f'Z/{modulus}[{variables} variables]/(variables)^2', + modulus**width, 1, add, mul) + + +def check_ring(r): + es = range(r.n) + require(r.one != 0, 'nonzero ring') + for a, b in product(es, repeat=2): + require(r.add[a][b] in es and r.mul[a][b] in es, 'closure') + require(r.add[a][b] == r.add[b][a] and r.mul[a][b] == r.mul[b][a], 'commutativity') + for a in es: + require(r.add[a][0] == a and r.mul[a][r.one] == a and r.mul[a][0] == 0, '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 local_data(r): + radical = tuple(x for x in range(r.n) if r.one not in r.mul[x]) + m = set(radical) + if r.one in m or any(r.add[x][y] not in m for x in m for y in m) or any( + r.mul[x][y] not in m for x in m for y in range(r.n)): + raise ValueError('the finite ring must be local') + generators = {r.mul[x][y] for x in m for y in m} + square = {0} + for g in generators: + principal = {r.mul[a][g] for a in range(r.n)} + square = {r.add[x][y] for x in square for y in principal} + covered, representatives = set(), [] + for x in range(r.n): + if x not in covered: + representatives.append(x) + covered.update(r.add[x][y] for y in m) + return radical, frozenset(square), tuple(representatives) + + +def validate_demand(r, d, data): + m, square, representatives = data + if len(d) != 3 or any(x not in m for x in d): + raise ValueError('three demands in the maximal ideal required') + for coefficients in product(representatives, repeat=3): + if coefficients == (0, 0, 0): + continue + value = 0 + for a, x in zip(coefficients, d): + value = r.add[value][r.mul[a][x]] + if value in square: + raise ValueError('demand classes must be independent modulo m^2') + + +def formula(mu, c): + if len(mu) != 3 or len(c) != 3 or min((*mu, *c)) <= 0: + raise ValueError('six strictly positive prices required') + values = [sum(mu)] + for k in range(3): + i, j = [r for r in range(3) if r != k] + values.append(2*mu[k]+2*c[i]+2*c[j]) + values.append(mu[i]+mu[j]+min(mu[i], mu[j])+2*c[k]) + return min(values) + + +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 i, j, k in permutations(range(3)): + v = [0]*6 + v[i], v[j], v[3+k] = 2, 1, 2 + out.append(('R', i, j, k, tuple(v))) + return out + + +def construct(r, d, pattern): + mode, i, j, k, _ = pattern + if mode == 'D': + return [(t, 3, d[t]) for t in range(3)] + u = r.add[d[i]][r.neg(r.one)] + if mode == 'T': + a = r.mul[d[k]][r.inv(u)] + return [(j, i, r.neg(d[j])), (i, 3, r.one), (j, i, d[j]), + (k, i, r.neg(a)), (i, 3, u), (k, i, a)] + if mode == 'R': + return [(k, i, r.neg(d[k])), (i, 3, r.one), (k, i, d[k]), + (i, 3, u), (j, 3, d[j])] + raise ValueError('unknown construction') + + +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): + rev = inverse(r, 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, rev, 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 R16 arithmetic: four 4-bit coefficients per 16-bit row. +# Multiplying the constant-bit mask by a radical digit cannot carry across +# 4-bit lanes. No coordinate ring tables, constructors or formula are used. +def packed_product(a, row): + return (row if a & 1 else 0) ^ ((a & 14)*(row & 0x1111)) + + +def neighbors(state, weights): + rows = [(state >> (16*i)) & 65535 for i in range(3)] + for i in range(3): + for a in range(1, 16): + yield state ^ (a << (16*i+12)), weights[i], (i, 3, a) + for j in range(3): + if j != i: + for a in range(1, 16): + yield state ^ (packed_product(a, rows[j]) << (16*i)), weights[3+i], (i, j, a) + + +def oracle(demand, prices): + 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 | (16 << 16) | (256 << 32) + goal = start | sum(x << (16*i+12) 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 + require(sum(settled) <= 50000 and len(ds[0])+len(ds[1]) <= 1000000, + 'oracle resource guard; query not certified') + for v, cost, gate in neighbors(u, weights): + 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) # All nonzero-coefficient primitives are involutions here. + return Fraction(best, scale), list(reversed(forward))+back, settled + + +def main(): + r16, r81, r64 = truncated_polynomials(2, 3), truncated_polynomials(3, 3), truncated_polynomials(4, 2) + pats = patterns() + vectors = [p[-1] for p in pats] + require(len(vectors) == len(set(vectors)) == 10, 'ten distinct envelope vectors') + total = dict(demands=0, words=0, formal_forward_inverse=0, literal_forward_inverse=0, + exposed_vectors=0, controls=0, oracle_queries=0, oracle_settled=0) + fixtures = [] + for r, expected in ((r16, 168), (r81, 11232), (r64, 10752)): + check_ring(r) + data = local_data(r) + accepted = 0 + for d in product(data[0], repeat=3): + try: + validate_demand(r, d, data) + except ValueError: + continue + accepted += 1 + for pat in pats: + word = construct(r, d, pat) + require(all(a != 0 and i != j for i, j, a in word), 'nonzero legal gates') + require(endpoint(r, d, word), 'constructed dirt endpoint/inverse') + require(counts(word) == pat[-1], 'claimed counts') + total['words'] += 1 + total['formal_forward_inverse'] += 8 + require(accepted == expected, 'exhaustive independent-class triple count') + total['demands'] += accepted + fixtures.append(dict(ring=r.name, independent_triples=accepted, maximal_ideal=len(data[0]), + square_ideal=len(data[1]), residue_field=len(data[2]))) + print('CHECK_RING', r.n, accepted, flush=True) + + d = (2, 4, 14) + words = [construct(r16, d, p) for p in pats] + for word in words: + rev = inverse(r16, word) + for entry in product(range(16), repeat=4): + want = target(r16, d, entry) + require(execute(r16, word, entry) == want and execute(r16, rev, want) == entry, + 'literal R16 forward/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)] + 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 envelope') + exposed.add(costs.index(minimum)) + require(len(exposed) == 10, 'all ten terms strictly exposed') + total['exposed_vectors'] = len(exposed) + for mu, c in product(range(1, 13), repeat=2): + require(formula((mu,)*3, (c,)*3) == min(3*mu, 2*mu+4*c), 'uniform-price specialization') + + # The lower rank zero-sum triple admits a cheaper predecessor M word. + rank_two = (2,4,6) + old_word = [(0,1,1), (2,0,1), (0,3,6), (1,3,4), (2,0,1), (0,1,1)] + prices = (3,5,10,1,3,2) + require(endpoint(r16, rank_two, old_word), 'rank-two predecessor word') + require(bill(old_word, prices) == 14 < formula(prices[:3], prices[3:]) == 15, + 'rank-three hypothesis is essential') + total['controls'] += 1 + for bad, fragment in [((0,4,14), 'independent'), (rank_two, 'independent'), + ((1,4,14), 'maximal ideal')]: + try: + validate_demand(r16, bad, local_data(r16)) + except ValueError as error: + require(fragment in str(error), 'correct hypothesis rejection') + total['controls'] += 1 + else: + raise RuntimeError('accepted demand outside theorem') + nonlocal_ring = ring_from_functions('F2 x F2', 4, 3, lambda x,y: x ^ y, lambda x,y: x & y) + check_ring(nonlocal_ring) + try: + local_data(nonlocal_ring) + except ValueError: + total['controls'] += 1 + else: + raise RuntimeError('accepted nonlocal ring') + corrupt = words[1][1:] + require(execute(r16, corrupt, (0,0,0,1)) == (*d,1), 'dirty-only corruption premise') + require(not endpoint(r16, d, corrupt), 'missing preparation must fail on dirt') + total['controls'] += 1 + d81 = (3,9,39) + bad_sign = construct(r81, d81, pats[1]) + i, j, a = bad_sign[0] + bad_sign[0] = (i, j, r81.neg(a)) + require(not endpoint(r81, d81, bad_sign), 'odd-characteristic sign control') + total['controls'] += 1 + d64 = (4,2,22) + bad_inverse = construct(r64, d64, pats[1]) + bad_inverse[3], bad_inverse[5] = (2,0,r64.neg(d64[2])), (2,0,d64[2]) + require(not endpoint(r64, d64, bad_inverse), 'unit inverse is necessary when m^2 is nonzero') + total['controls'] += 1 + relator = [(0,1,1), (1,2,1), (0,1,1), (1,2,1), (0,2,1)] + require(endpoint(r16, (0,0,0), relator), 'three-row identity control') + require(sum((i,j) == (0,2) for i,j,_ in relator) == 1, 'row-return lemma is not per edge') + 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 prices') + + for a in range(16): + for row in range(65536): + expected = sum(r16.mul[a][(row >> (4*k)) & 15] << (4*k) for k in range(4)) + require(packed_product(a, row) == expected, 'independent packed arithmetic') + cases = [('D', (1,1,1,1,1,1)), ('T', (1,10,10,10,1,1)), + ('R', (1,2,10,10,10,1)), + ('rational', (Fraction(1,2),Fraction(2,3),Fraction(3,4), + Fraction(1),Fraction(4,3),Fraction(5,4)))] + results = [] + for name, prices in cases: + value, path, settled = oracle(d, prices) + require(value == formula(prices[:3], prices[3:]), f'oracle mismatch: {name}') + require(endpoint(r16, d, path) and bill(path, prices) == value, 'oracle path replay and bill') + 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), settled, flush=True) + print(json.dumps(dict(fixtures=fixtures, counts=total, oracle=results), sort_keys=True)) + print('PASS_R16_RADICAL_TRIPLE_FANOUT no_new_kappa') + + +if __name__ == '__main__': + main()