Prove a principal-ideal dirty-fanout obstruction over K[x,y] (no new κ)

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.

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.

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.

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"
+    }
+  ]
+}