diff --git a/research/cohn-fanout-obstruction/PROOF.md b/research/cohn-fanout-obstruction/PROOF.md new file mode 100644 index 0000000000..fd28405187 --- /dev/null +++ b/research/cohn-fanout-obstruction/PROOF.md @@ -0,0 +1,150 @@ +# Polynomial dirty fanout with a unit demand ideal + +## Contract and statement + +Let K be any commutative field and R=K[x,y], with commuting indeterminates. +There are two arbitrary dirty rows a0,a1 in R^w and a disjoint preserved +source p in R^w, where w>=1. A fixed finite straight-line word must realize + + (a0,a1,p) -> (a0+(1+xy)p, a1+x²p, p) + +for every input. The only gates are + + P_i(beta): A_i <- A_i + beta p, price mu_i > 0; + E_i(alpha): A_i <- A_i + alpha A_(1-i), price c_i > 0. + +Here i is 0 or 1, alpha and beta are arbitrary elements of R, and c_i +charges the direction into row i. Prices are stationary, inclusive abstract +prices and independent of coefficient. There are no extra rows, free basis +changes, observations, clearing or input-dependent choices. Every original +dirt column must return exactly. An inverse execution is charged separately. +This is the contract of #5045/#5139, with a polynomial coefficient ring. + +**Theorem.** The demand ideal is R, but no legal word has exactly one +nonzero source insertion. The exact all-positive-price optimum is + + min(mu0+mu1, 2mu0+2c1, 2mu1+2c0). + +The exact Pareto-minimal count vectors in order (P0,P1,E0,E1) are + + (1,1,0,0), (2,0,0,2), (0,2,2,0). + +The statement includes characteristic two. It is a scoped algebraic result, +not a native supplier or a complete multiplication theorem. + +## The inherited theorem + +We use Cohn's classical example, without reproving or auditing it: + + C = [[1+xy, x²], [-y², 1-xy]] is not in E2(K[x,y]). + +Here E2 is the group generated by upper and lower elementary shears. +The source is P. M. Cohn, *On the structure of the GL2 of a ring*, +Publications Mathématiques de l'IHÉS 30, 1966, pp. 5-53, §7, printed +p. 26, unnumbered example after Proposition 7.3. See +[the primary example](https://www.numdam.org/item/PMIHES_1966__30__5_0.pdf#page=23) +and [REFERENCES.md](REFERENCES.md). Cohn excludes the larger group GE2; +only the displayed E2 consequence is used. His field hypothesis has no +characteristic restriction. This theorem is an explicit cited dependency, +not a machine-certified conclusion of this package. + +## From one insertion to an elementary column + +Write lambda=(1+xy,x²)^T and A=C^T. The integer polynomial identity + + (1-xy)(1+xy) + y² x² = 1 + +shows that lambda is unimodular, so its entries generate R. Also det A=1. + +Suppose a legal word has just one nonzero insertion P_i(beta). Delete any +zero-coefficient gates, which have positive price and no effect. Let Q be +the product of the row gates after that insertion, in execution order. +Before the insertion the source column is zero; afterward it is + + lambda = beta Q e_i, Q in E2(R). + +A column of an invertible matrix is unimodular, so the ideal generated by +beta Q e_i is (beta). Since lambda generates R, beta is a unit. + +Both coordinate columns e_i lie in the E2 orbit of e0. For e1 use +J=[[0,-1],[1,0]], a product of three elementary shears. For a unit b, +diag(b,b^-1) is elementary: with U(t) upper and L(t) lower, + + U(b)L(-b^-1)U(b) U(-1)L(1)U(-1) = diag(b,b^-1). + +Consequently Q J_i diag(beta,beta^-1) is an elementary determinant-one +matrix H whose first column is lambda. Here J_0=I and J_1=J. + +But every determinant-one completion H of this column has + + A^-1 H = [[1,t],[0,1]] + +for some t in R: the first column is e0 and the determinant is one. +Thus H=A U(t). If H were elementary, A=H U(-t) would be elementary. +Transposition preserves E2, since it transposes each shear and reverses +the order of a product. This would make C elementary, contradicting the +cited theorem. Hence exactly one nonzero insertion is impossible at +either row, for words of any finite length and coefficients of any degree. + +This is the new consequence of the classical example. It answers +Open next question 1 in lee-phys's #5139: principality, even the unit ideal, +does not suffice beyond its finite-commutative-ring domain. + +## Arbitrary-word lower bound + +We use Krzysztof Wójt's #5045 directional return and source-count argument. +For completeness its short application follows. Set p=0 and track the two +independent original dirt columns. The product of row gates must be I2. +If a nonzero upper shear occurs exactly once, all lower shears before it +and after it combine, giving L(s)U(alpha)L(t). Its upper-right entry is +alpha, so it is not I2. Swapping rows gives the other direction. Every +used direction therefore occurs at least twice. Source gates do not +affect this dirt argument. + +There is at least one insertion, since row gates alone leave the source +column zero. The previous section excludes exactly one. If both rows +receive insertions, the count vector dominates (1,1,0,0). Otherwise only +row i receives insertions, at least twice. The nonzero demand in row j +requires a row gate into j, hence at least two such gates by the return +lemma. Its counts dominate (2,0,0,2) or (0,2,2,0). These cases exhaust all +finite words, regardless of interleaving or cancellation. They prove the +claimed lower envelope for every positive price vector. + +## Matching constructions + +Put u=1+xy and v=x². The following words are in chronological order. +They are #5045's direct and repeated-insertion templates applied to this +new polynomial demand. + + D: P0(u), P1(v) + T0: E1(-1), P0(v), E1(1), P0(u-v) + T1: E0(-1), P1(u), E0(1), P1(v-u) + +Each word has the required complete affine endpoint, including both dirt +columns and the source row. In T0, the first row gates cancel on dirt; +the first insertion transfers v to row 1, then the last insertion leaves +u at row 0. The row-swapped argument proves T1. Every displayed gate has +nonzero polynomial coefficient over every field, including characteristic +two. Their costs are the three entries of the theorem. + +The three vectors are incomparable and each is strictly cheapest at some +positive prices. In price order (mu0,mu1,c0,c1), examples are (1,1,1,1), +(1,10,1,1), and (10,1,1,1), respectively. Since every word dominates one +of them, these are exactly the Pareto-minimal count vectors. + +## What the finite checks establish + +The verifier checks the Bezout identity and both inverses of A as exact +integer polynomial identities. It multiplies every complete affine word, +its inverse, and ten one-call deletions. Six completion fixtures +corroborate the coset identity; its general proof is above. A changed +alphabet control conjugates one insertion by the full A and attains the +target, exposing the essential restriction to elementary row gates. + +For all x,y and all three scalar data values over F2,F3,F5,F7, it checks +every attaining word and inverse. All 87 evaluated demand pairs also +have explicit one-insertion words over their finite fields. Thus these +evaluations cannot witness polynomial non-elementarity. The obstruction +uses the cited infinite-ring theorem, not an extrapolation from a bounded +word search or a finite-ring failure. No predecessor verifier is imported +or replayed. diff --git a/research/cohn-fanout-obstruction/README.md b/research/cohn-fanout-obstruction/README.md new file mode 100644 index 0000000000..831e465aa7 --- /dev/null +++ b/research/cohn-fanout-obstruction/README.md @@ -0,0 +1,132 @@ +# A unit demand ideal does not guarantee one-insertion fanout + +Scoped algebraic proof with exact finite corroboration. This contribution +was produced by Nick Petalas. Apache-2.0. + +For every field K, the polynomial demand pair `(1+xy,x²)` over K[x,y] +generates the whole ring, but no two-row dirty-fanout word can realize it +with a single nonzero source insertion. This answers Open next question 1 +of lee-phys's [#5139](https://github.com/CrocSwap/integer-mult-bounds/pull/5139). +Its finite-commutative-ring theorem remains a cited predecessor. The new +step is the fanout consequence of Cohn's classical elementary-matrix +obstruction, followed by the matching exact tariff. + +With positive stationary coefficient-independent insertion prices mu0,mu1 +and row-addition prices c0,c1, the exact optimum is + +```text +min(mu0+mu1, 2mu0+2c1, 2mu1+2c0). +``` + +The contract has exactly two arbitrary dirty output rows and one disjoint +preserved source. Gates are polynomial source insertions and elementary +row additions, priced into their destination row. Both dirt columns must +return, and there are no extra rows or free general linear maps. +[PROOF.md](PROOF.md) gives the full contract and all-word proof, including +the three exact Pareto-minimal count vectors and restoring words. The +statement includes characteristic two and every positive data width. + +## Evidence + +The standard-library verifier checks exact integer polynomial Bezout, +inverse, affine-endpoint and completion-coset identities. It checks three +attaining words and all ten individual call deletions. It enumerates +60,621 forward/inverse scalar-input pairs over F2,F3,F5,F7 and 625 positive +integer price vectors. Seventeen controls cover omissions, order, invalid +domains, false polynomial division and the changed alphabet that grants +the entire Cohn matrix as a row gate. + +Every one of the 87 field-evaluated demand pairs has a checked +one-insertion word. Those finite specializations cannot establish the +polynomial obstruction. The lower bound uses Cohn's **cited** theorem, +not a finite search or a machine verification of that theorem. The +verifier explicitly records that distinction in its generated receipt. +It writes nothing and binds every package source file by SHA256. + +## Reproduce + +From the repository root, using the CPython 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/cohn-fanout-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/cohn-fanout-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cohn-fanout-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cohn-fanout-obstruction --check-source-history +``` + +Another CPython 3.12 installation can replace the local interpreter path. +Expected direct marker: + +```text +PASS_COHN_FANOUT scalar_pairs=60621 specializations=87 prices=625 controls=17 no_new_kappa +``` + +Both registered checks have 120-second limits. Normal and optimized checks +remain active because the verifier uses explicit exceptions. Its direct +replay also supports a Git-free package export. + +## Scope and provenance + +The original `bit-helper-contract` card is explicitly changed to #5139's +algebraic interface question in [TASK.json](TASK.json). This is a local +obstruction, not an admission claim for the original helper-star circuit. +Base is canonical main `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority +revision 7. [SOURCES.json](SOURCES.json) pins predecessor proof text as +historical provenance. No predecessor code or verifier is imported or +replayed. Selected source-binding orientation passed; the selected +conditional kappa remains 60403/20000000. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145584) +followed live PR/Discussion checks, cached card overlap and distinctive +main-tree/merged-PR searches. Cached remote pagination covered 315 open +PRs and 4,395 Discussion records. Local coverage was sparse and incomplete; +these searches cannot exclude unpublished or later work. + +## Limits and code constraints + +The universal obstruction is the written reduction to Cohn's theorem. +Its non-elementarity premise is a classical cited result, inherited +without an audit or proof-kernel verification. The finite checks +corroborate only their stated identities and domains. The coefficient +ring, elementary gate alphabet and exact two-row contract matter. +Additional workspace, clearing, observations, general free basis maps +and input-dependent coefficients are excluded. + +No native coefficient producer, physical routing, restoration tariff, +precision/tape implementation, stock, recursive supplier, new kappa or +complete multiplication theorem is supplied. Lean, Docker and the selected +scientific cold replay are outside scope and were not run. Independent +human and formal proof-kernel review are unclaimed. + +The verifier has no recursion, subprocess, network or write path. Its +functions are below 60 lines, matrices have three rows, word length is +at most eight, field sizes are at most seven, and the price grid has +5^4 points. Polynomial operations enforce at most 289 temporary terms +and exponent at most 16 in either variable. The receipt reads at most +12 files of at most 128 KiB each. Python dynamically allocates within +these fixed finite domains, a managed-runtime deviation from static +allocation. Runtime allocator internals are not measured. Warning-strict +normal/optimized replay and in-memory compilation supply the available +diagnostics; no shared build or verifier settings change. + +## Credit + +Paul M. Cohn supplies the classical non-elementary matrix. Its exact +primary-source location and characteristic scope are in +[REFERENCES.md](REFERENCES.md). No novelty is claimed for that theorem. +lee-phys #5139 supplies the finite-commutative-ring criterion and the +explicit nonsemilocal elementary-orbit question, building on #5089. +Krzysztof Wójt #5045 supplies the source-count classification, +directional return lemma and attaining repeated-insertion templates. +Nick Petalas #4916 supplies the earlier ring-valued contract. Retain the +Ross Richardson, Cinna Davis, Anthony, Oscar Fennell, Tekalign and other +predecessor credit recorded in those packages. Their files are unchanged. + +## Open next questions + +Can one extra restored dirty row remove this polynomial one-insertion +obstruction, and at what complete price? Start with a stabilized Cohn +matrix, retaining all three independent dirt columns and all paid row +directions. This would separate two-row elementary reachability from +stabilized reachability. A fully charged restoring word and matching +tariff remain unproved here. No further construction is claimed. diff --git a/research/cohn-fanout-obstruction/REFERENCES.md b/research/cohn-fanout-obstruction/REFERENCES.md new file mode 100644 index 0000000000..0319d955c1 --- /dev/null +++ b/research/cohn-fanout-obstruction/REFERENCES.md @@ -0,0 +1,35 @@ +# References + +Paul M. Cohn, "On the structure of the GL₂ of a ring," *Publications +Mathématiques de l'Institut des Hautes Études Scientifiques* **30**, +1966, pp. 5-53. DOI: [10.1007/BF02684355](https://doi.org/10.1007/BF02684355). +[Publisher metadata](https://www.numdam.org/item/PMIHES_1966__30__5_0/). +[Primary PDF](https://www.numdam.org/item/PMIHES_1966__30__5_0.pdf). + +The exact example is in §7, printed p. 26, immediately after Proposition 7.3 +and before §8. It is unnumbered, not Proposition 7.4. In the linked PDF this +is page index 22, the 23rd PDF page, also bearing the footer 386. +[Open that page](https://www.numdam.org/item/PMIHES_1966__30__5_0.pdf#page=23). + +For every commutative field $K$, with commuting indeterminates $x,y$, the +inherited statement is + +$$ +C=\begin{pmatrix}1+xy&x^2\\-y^2&1-xy\end{pmatrix} +\in \operatorname{SL}_2(K[x,y])\setminus E_2(K[x,y]). +$$ + +Here $E_2(R)$ is generated by $I+f e_{12}$ and $I+f e_{21}$ for $f\in R$. +Cohn identifies this group in §2, printed p. 7. His example states the +stronger exclusion from $\operatorname{GE}_2$, whose elementary generators +also include invertible diagonal matrices. The example uses total degree +on $K[x,y]$. Neither its field hypothesis nor Proposition 7.3 excludes +characteristic 2. Thus characteristic 2 is included in the general +statement, although Cohn gives no separate characteristic-2 corollary. + +Bibliographic confidence is high. The displayed matrix and location were +checked against the primary facsimile, and the publication data against +Numdam's record. The non-elementarity result is Cohn's classical theorem, +inherited without a new proof or an audit of his theorem. This package is +prepared by Nick Petalas. No independent human or proof-kernel review is +claimed. diff --git a/research/cohn-fanout-obstruction/SOURCES.json b/research/cohn-fanout-obstruction/SOURCES.json new file mode 100644 index 0000000000..dc85264ce7 --- /dev/null +++ b/research/cohn-fanout-obstruction/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "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/two-row-nonunit-fanout/PROOF.md", + "usage": "provenance", + "git_blob": "1bd3b47624db83c45ca08fb498f2a84d814306c1", + "sha256": "d177967c73bd5e755c5f70964d5542420e23e36cad81c57452a222e50e356f77" + } + ] +} diff --git a/research/cohn-fanout-obstruction/TASK.json b/research/cohn-fanout-obstruction/TASK.json new file mode 100644 index 0000000000..c8b75222c3 --- /dev/null +++ b/research/cohn-fanout-obstruction/TASK.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "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": "Exclude one source insertion for the unimodular demand (1+xy,x^2) over every K[x,y] and prove its exact two-row all-positive-price dirty-fanout tariff.", + "scope_change_reason": "Take Open next question 1 of lee-phys PR5139 on nonsemilocal elementary-column reachability; this is an algebraic side result rather than a new H2/K helper-star supplier.", + "bottleneck_link": "A principal demand ideal alone cannot justify a cheaper one-insertion dirty-helper interface. This scoped obstruction identifies a missing elementary-reachability premise; physical supplier costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved obstruction and matching tariff; do not extend the construction or replay predecessor results.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-word argument using the cited Cohn theorem. verify.py checks exact polynomial identities, 60621 forward/inverse scalar pairs, 87 field-specialization one-insertion witnesses, 625 price vectors and 17 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one extra restored dirty row remove this polynomial one-insertion obstruction, at what complete price?", + "why_it_matters": "Separates two-row elementary reachability from stabilized reachability and tests which paid premise changes.", + "first_step": "Construct a stabilized Cohn elementary word and retain all three independent dirt columns and every paid row direction.", + "blocked_by": "No fully charged three-row restoring construction or sharp tariff is proved here." + } + ] +} diff --git a/research/cohn-fanout-obstruction/VERIFY.json b/research/cohn-fanout-obstruction/VERIFY.json new file mode 100644 index 0000000000..6a9eb089af --- /dev/null +++ b/research/cohn-fanout-obstruction/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact polynomial identities, complete dirty/source endpoints, inverse and omission controls, all stated field inputs, price invoices and explicit classical-theorem boundary." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All scientific and rejection checks remain enabled under optimization." + } + ] +} diff --git a/research/cohn-fanout-obstruction/verify.py b/research/cohn-fanout-obstruction/verify.py new file mode 100644 index 0000000000..ccc38994a3 --- /dev/null +++ b/research/cohn-fanout-obstruction/verify.py @@ -0,0 +1,267 @@ +#!/usr/bin/env python3 +"""Exact identities for polynomial dirty fanout; Cohn's theorem is cited.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +MAX_EXPONENT = 16 +MAX_TERMS = 289 +MAX_WORD = 8 +PRIMES = (2, 3, 5, 7) +ZERO = () +ONE = ((0, 0, 1),) +X = ((1, 0, 1),) +Y = ((0, 1, 1),) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def polynomial(terms): + require(len(terms) <= MAX_TERMS, "polynomial input capacity") + merged = {} + for x, y, coefficient in terms: + require(0 <= x <= MAX_EXPONENT and 0 <= y <= MAX_EXPONENT, + "polynomial exponent capacity") + require(type(coefficient) is int and coefficient.bit_length() <= 64, + "integer coefficient capacity") + merged[x, y] = merged.get((x, y), 0) + coefficient + result = tuple((x, y, c) for (x, y), c in sorted(merged.items()) if c) + require(len(result) <= MAX_TERMS, "polynomial output capacity") + require(all(c.bit_length() <= 64 for _, _, c in result), + "polynomial output coefficient capacity") + return result + + +def add(a, b): + require(len(a) + len(b) <= MAX_TERMS, "addition capacity") + return polynomial(a + b) + + +def neg(a): + return tuple((x, y, -c) for x, y, c in a) + + +def multiply(a, b): + require(len(a) * len(b) <= MAX_TERMS, "multiplication capacity") + return polynomial(tuple((x + u, y + v, c * d) + for x, y, c in a for u, v, d in b)) + + +def evaluate(a, x, y, prime): + require(prime in PRIMES and 0 <= x < prime and 0 <= y < prime, + "field evaluation domain") + return sum(c * pow(x, u, prime) * pow(y, v, prime) + for u, v, c in a) % prime + + +def identity(): + return tuple(tuple(ONE if i == j else ZERO for j in range(3)) + for i in range(3)) + + +def matrix_product(a, b): + require(len(a) == len(b) == 3, "three-row matrix domain") + rows = [] + for i in range(3): + row = [] + for j in range(3): + entry = ZERO + for k in range(3): + entry = add(entry, multiply(a[i][k], b[k][j])) + row.append(entry) + rows.append(tuple(row)) + return tuple(rows) + + +def gate(kind, row, coefficient): + require(kind in ("P", "E") and row in (0, 1), "gate domain") + result = [list(r) for r in identity()] + result[row][2 if kind == "P" else 1 - row] = coefficient + return tuple(tuple(r) for r in result) + + +def endpoint(word): + require(len(word) <= MAX_WORD, "word capacity") + result = identity() + for kind, row, coefficient in word: + result = matrix_product(gate(kind, row, coefficient), result) + return result + + +def inverse_word(word): + require(len(word) <= MAX_WORD, "inverse word capacity") + return tuple((kind, row, neg(c)) for kind, row, c in reversed(word)) + + +def fixture(): + xy = multiply(X, Y) + x2, y2 = multiply(X, X), multiply(Y, Y) + demand = (add(ONE, xy), x2) + cohn_transpose = ((demand[0], neg(y2), ZERO), + (x2, add(ONE, neg(xy)), ZERO), + (ZERO, ZERO, ONE)) + cohn_inverse = ((add(ONE, neg(xy)), y2, ZERO), + (neg(x2), demand[0], ZERO), + (ZERO, ZERO, ONE)) + target = ((ONE, ZERO, demand[0]), (ZERO, ONE, demand[1]), + (ZERO, ZERO, ONE)) + return demand, cohn_transpose, cohn_inverse, target + + +def candidates(demand): + x, y = demand + direct = (("P", 0, x), ("P", 1, y)) + into_zero = (("E", 1, neg(ONE)), ("P", 0, y), + ("E", 1, ONE), ("P", 0, add(x, neg(y)))) + into_one = (("E", 0, neg(ONE)), ("P", 1, x), + ("E", 0, ONE), ("P", 1, add(y, neg(x)))) + return direct, into_zero, into_one + + +def counts(word): + return tuple(sum(kind == k and row == r for kind, row, _ in word) + for k, r in (("P", 0), ("P", 1), ("E", 0), ("E", 1))) + + +def scalar_execution(word, values, x, y, prime): + result = list(values) + for kind, row, coefficient in word: + source = 2 if kind == "P" else 1 - row + result[row] = (result[row] + evaluate(coefficient, x, y, prime) + * result[source]) % prime + return tuple(result) + + +def identities_and_controls(): + demand, cohn, cohn_inverse, target = fixture() + require(matrix_product(cohn, cohn_inverse) == identity(), "Cohn inverse") + require(matrix_product(cohn_inverse, cohn) == identity(), "left inverse") + bezout = add(multiply(demand[0], cohn[1][1]), + multiply(demand[1], multiply(Y, Y))) + require(bezout == ONE, "unimodular demand identity") + controls = 0 + words = candidates(demand) + expected_counts = ((1, 1, 0, 0), (2, 0, 0, 2), (0, 2, 2, 0)) + for word, expected in zip(words, expected_counts): + require(counts(word) == expected, "candidate counts") + require(endpoint(word) == target, "complete affine endpoint") + require(matrix_product(endpoint(inverse_word(word)), target) == identity(), + "inverse restores source and arbitrary dirt") + for removed in range(len(word)): + require(endpoint(word[:removed] + word[removed + 1:]) != target, + "single deletion must fail") + controls += 1 + # An arbitrary SL2 row gate defeats the obstruction. It is not free. + relaxed = matrix_product(cohn, matrix_product(gate("P", 0, ONE), cohn_inverse)) + require(relaxed == target, "changed-alphabet control") + require(endpoint(tuple(reversed(words[1]))) != target, "order control") + naive = (("E", 1, neg(demand[1])), ("P", 0, demand[0]), + ("E", 1, demand[1])) + require(endpoint(naive) != target, "false polynomial division control") + controls += 3 + for t in (ZERO, ONE, X, Y, add(X, Y), multiply(X, Y)): + completion = matrix_product(cohn, gate("E", 0, t)) + require(tuple(completion[i][0] for i in range(2)) == demand, + "completion column") + require(matrix_product(cohn_inverse, completion) == gate("E", 0, t), + "completion coset identity") + return words, controls + + +def specializations(words): + demand, _, _, _ = fixture() + scalar_checks, one_insertions = 0, 0 + for prime in PRIMES: + for x, y in itertools.product(range(prime), repeat=2): + a, b = (evaluate(c, x, y, prime) for c in demand) + require(a != 0 or b != 0, "specialized demand is unimodular") + # Every field specialization DOES have a one-insertion word. + alpha = 0 if a else 1 + beta = (a - alpha * b) % prime + r = b * pow(beta, -1, prime) % prime + scalar_word = (("E", 0, polynomial(((0, 0, -alpha),))), + ("E", 1, polynomial(((0, 0, -r),))), + ("P", 0, polynomial(((0, 0, beta),))), + ("E", 1, polynomial(((0, 0, r),))), + ("E", 0, polynomial(((0, 0, alpha),)))) + for basis in ((1, 0, 0), (0, 1, 0), (0, 0, 1)): + expected = ((basis[0] + a * basis[2]) % prime, + (basis[1] + b * basis[2]) % prime, basis[2]) + require(scalar_execution(scalar_word, basis, x, y, prime) == expected, + "field specialization one-insertion witness") + one_insertions += 1 + for values in itertools.product(range(prime), repeat=3): + expected = ((values[0] + a * values[2]) % prime, + (values[1] + b * values[2]) % prime, values[2]) + for word in words: + actual = scalar_execution(word, values, x, y, prime) + require(actual == expected, "arbitrary scalar input") + require(scalar_execution(inverse_word(word), actual, x, y, prime) + == values, "arbitrary scalar inverse") + scalar_checks += 1 + return scalar_checks, one_insertions + + +def price_checks(words): + vectors = tuple(counts(word) for word in words) + comparisons = 0 + for prices in itertools.product(range(1, 6), repeat=4): + measured = tuple(sum(a * b for a, b in zip(v, prices)) for v in vectors) + mu0, mu1, c0, c1 = prices + formula = (mu0 + mu1, 2 * mu0 + 2 * c1, 2 * mu1 + 2 * c0) + require(measured == formula, "complete candidate invoice") + comparisons += 1 + for winner, prices in enumerate(((1, 1, 1, 1), (1, 10, 1, 1), (10, 1, 1, 1))): + costs = tuple(sum(a * b for a, b in zip(v, prices)) for v in vectors) + require(all(costs[winner] < costs[j] for j in range(3) if j != winner), + "each Pareto vector has a strict positive-price witness") + return comparisons + + +def boundary_controls(): + rejected = 0 + for terms in (((17, 0, 1),), ((0, 0, True),), ((0, 0, 1 << 65),)): + try: + polynomial(terms) + except ValueError: + rejected += 1 + try: + evaluate(ONE, 0, 0, 4) + except ValueError: + rejected += 1 + require(rejected == 4, "invalid domains must reject") + return rejected + + +def main(): + words, controls = identities_and_controls() + scalar_checks, one_insertions = specializations(words) + prices = price_checks(words) + controls += boundary_controls() + package = Path(__file__).resolve().parent + files = sorted(p for p in package.iterdir() if p.suffix in (".py", ".md", ".json")) + require(len(files) <= 12, "receipt file capacity") + hashes = {} + for path in files: + with path.open("rb") as stream: + data = stream.read(131073) + require(len(data) <= 131072, "receipt file byte capacity") + hashes[path.name] = hashlib.sha256(data).hexdigest() + receipt = {"claim_type": "scoped proof using cited Cohn theorem", + "scalar_forward_inverse_pairs": scalar_checks, + "field_specializations_with_one_insertion": one_insertions, + "price_vectors": prices, "controls": controls, + "cohn_non_elementarity_machine_verified": False, "sha256": hashes} + print(json.dumps(receipt, sort_keys=True)) + print(f"PASS_COHN_FANOUT scalar_pairs={scalar_checks} " + f"specializations={one_insertions} prices={prices} controls={controls} no_new_kappa") + + +if __name__ == "__main__": + main()