Prove a single-owner obstruction to staggered fresh-feed repair

research/staggered-single-owner-obstruction/README.md

@@ -0,0 +1,228 @@
+# A single-owner obstruction to fresh-feed repair of the staggered prefix
+
+**A uniform-word obstruction, not a general small-unit lower bound.** In the
+five-call staggered preparation of Yiyang's
+[continuation handoff](https://github.com/Lyy-iiis/integer-mult-bounds/tree/dcd20b2112327d903babbddc654a535dcfdb1b63/research/phase-prefix-continuations),
+changing only the fresh-owner feed cannot create a nonzero pure-target channel.
+This includes all fourteen `Π±,f=(I±X_a^⊗f)/2` feeds with nonzero three-bit `a`,
+while retaining the independent complementary input. In fact, the result holds
+for **every uniform free feed B**, without an invertibility assumption on B.
+
+The new certificate sees only the original `x` input. Six retained registers
+have a triangular, invertible coefficient matrix on six low-order left cosets.
+The old two-owner graph screen used a unit on the fresh `y` side; replacing that
+unit by a projector could invalidate that particular screen. The new screen
+remains unchanged because it ignores the `y` coefficients entirely. Thus this
+proposed change does not exploit the missing kernel-bearing interface.
+
+This closes the claimed fresh-feed scaffold and advises changing the original
+`x` chronology before further construction. It does not exclude different
+five-call preparations, general five-in-fourteen or six-in-seventeen programs,
+fixed-width identities, or width-dependent scalar decoders. No κ or selected
+frontier changes.
+
+## Exact program and model
+
+Use the predecessor's eight-dimensional base matrices, with words acting
+right to left. `C_j=((1+i)I+(1-i)X_j)/2`, `K=C_0 C_1 C_2`, and
+`S e_x=i^popcount(x)e_x`. Let `U=CNOT(0→2)`, `V=SWAP01`, `T=SWAP02`, and
+
+```
+P = S U S                 Q = S V S
+Q2 = S SWAP21 S           W = Z0 Z2
+N = Z1 V                 J = N C2          L = N T.
+```
+
+For a base word `g`, write `g_f=g^⊗f`. Each base word is tensorized **before**
+forming sums, whose scalar coefficients stay independent of positive width f.
+For any free uniform operator `B_f`, retain `x,y` and execute
+
+```
+u = C0_f x
+v = C0_f (P_f + 2 Q_f) u
+r = L_f^-1 J_f (W_f v + T_f B_f y)
+t = C0_f (P_f + 2 Q_f) r
+z = J_f (W_f t + Q2_f r + P_f v).
+```
+
+Each displayed line costs one call. `J_f` is a free monomial followed by one
+`C2_f` call. All free intermediates and arbitrary extra zero scratch are
+allowed. Keeping all seven registers strengthens the decoder, even if a real
+implementation would overwrite some. Free copies and mixtures of retained
+registers are allowed without restriction in the enlarged free group below.
+The theorem does not treat an unrelated transformed `y` supplied by an oracle
+as a free input.
+
+### Uniform-word algebra is not a width-one matrix algebra
+
+Let H be **all** 8×8 monomial matrices with fourth-root entries, retaining
+central phases, and A=ℂ[H]. H is finite and contains the actual free letters.
+Let G be the group of actual base matrices generated by H and the paid letters.
+G need not be finite. A uniform word is a finite element of ℂ[G], evaluated at
+width f by sending each actual matrix g to `g^⊗f`. The feed B belongs to A.
+A decoder may use any coefficients in A on all retained registers. This
+enlarges the actual engine, so its obstruction also applies to the original
+free alphabet. Scalar mixing may be complex, but is fixed across widths.
+
+**Separation lemma (retained from the predecessor).** Distinct actual matrices
+`g_1,...,g_n` are linearly independent as the families `(g_i^⊗f)_(f≥1)`.
+Choose a complex linear functional ℓ whose values on these matrices are
+nonzero and pairwise distinct; the excluded choices are finitely many proper
+hyperplanes. Applying `ℓ^⊗f` for f=1,...,n to a uniform relation gives an
+invertible Vandermonde matrix (with an additional nonzero diagonal factor).
+Every coefficient therefore vanishes. Distinct global phases are not
+identified. Consequently a claimed identity at every positive width is an
+identity in ℂ[G]; an identity at width one alone is insufficient.
+
+Partition G into left cosets Hh. Their spans are independent copies of the
+left A-module A. Projection onto any collection of left cosets commutes with
+arbitrary free left processing. Exact base-matrix tests `g h^-1∈H` establish
+membership in these **defined groups**, rather than extrapolating a finite
+numeric rank to a statement about all widths.
+
+## New triangular certificate
+
+Put `A0=L^-1 J W` and define the single-word representatives
+
+```
+R4 = C0 P C0
+R6 = C0 P A0 C0 Q C0
+R7 = C0 Q A0 C0 P C0.
+```
+
+`I,C0,R4,C2,R7,R6,K` belong to seven distinct left H-cosets. The exact checker
+verifies all 21 separating pairs over Gaussian rationals. Project the **x
+coefficient only** onto the ordered six cosets
+
+```
+HI, HC0, HR4, HC2, HR7, HR6.
+```
+
+Order the six registers as `x,u,v,r,z,t`. Their coefficient matrix is
+
+| Register | HI | HC0 | HR4 | HC2 | HR7 | HR6 |
+|---|---:|---:|---:|---:|---:|---:|
+| x | 1 | 0 | 0 | 0 | 0 | 0 |
+| u | 0 | 1 | 0 | 0 | 0 | 0 |
+| v | 0 | 0 | 1 | 0 | 0 | 0 |
+| r | 0 | 0 | 0 | U0 | 0 | 0 |
+| z | 0 | * | 0 | * | D | 0 |
+| t | * | 0 | 0 | 0 | * | 2 |
+
+The starred coefficients are explicit finite elements of A, not assumed zero.
+`U0` is a monomial unit. All coefficient words, including the starred cells,
+are recorded in [RESULT.json](RESULT.json). Neither the table nor its proof
+depends on B: every changed feed is supported only on y.
+
+The only nontrivial diagonal is `D=g1+2g2`, where the fourth-root monomials are
+specified by output row and phase exponent for input columns 0,...,7:
+
+```
+g1 permutation: 0 4 2 6 1 5 3 7    phases: 0 0 2 2 0 0 2 2
+g2 permutation: 1 0 7 6 5 4 3 2    phases: 3 1 0 2 3 1 2 0.
+```
+
+For `R=g1^-1 g2`, exact multiplication gives order four. In A,
+
+```
+(I+2R)(I-2R+4R²-8R³) = -15 I,
+D^-1 = -(I-2R+4R²-8R³)g1^-1/15.
+```
+
+This is checked coefficientwise in the group algebra, as well as on the base
+matrices. The identity tensorizes term by term with the same scalar
+coefficients at every width. Thus every diagonal of the triangular table is
+a unit in A; no commutativity assumption on A is needed.
+
+### Decoder consequence
+
+Suppose an arbitrary free mixture of retained registers is a pure target
+`a K x + b K y`, with a,b∈A. Its six projected x coefficients vanish because
+HK is distinct from every chosen coset. In the table, the HR6 column first
+forces the coefficient of t to vanish; HR7 then forces the coefficient of z
+to vanish; HC2, HR4, HC0 and HI successively force those of r,v,u,x to vanish.
+This is elimination over A using the explicit units, not a ban on free
+mixtures. The only remaining retained input is a free multiple of y. Its
+coefficient lies in H, whereas a pure target lies in HK. Coset independence
+forces that remaining coefficient and a,b to vanish as well.
+
+Therefore the retained A-span intersects the pure two-target module only in
+zero, for every B∈A. The two target directions have dimension `2 dim(A)`.
+One further paid call creates at most one new A-generator, increasing the
+span by at most `dim(A)`, regardless of free copies or mixing. **At least two
+additional calls are necessary after this five-call preparation.** This
+extends the predecessor's endpoint conclusion across the whole fresh-feed
+class. It does not prevent other preparations from using six calls for two
+arrays, and supplies no global small-unit lower bound.
+
+## Evidence, scope and decision
+
+The written argument supplies the quantifiers. The checker authenticates and
+compiles the retained arithmetic bytes, expands the actual program as finite
+sums of distinct actual base words, verifies the triangular table and every
+coset separation, and checks the unit inverse in the group algebra. It also
+checks all fourteen originally claimed projector feeds and exact recovery of
+their complements. The receipt is deterministic and does not regenerate by
+default. Five controls cover missing pivots, replacing a residual by a target,
+the singular coefficient-one pencil, the failure of a width-one identity to
+tensorize as a sum, and central-phase separation.
+
+The family decision is **stop fresh-feed-only repair**. The five paid calls,
+free feed/decoder allowance and two further-call necessity are proved in the
+uniform word model. Physical storage, routing, precision and full supplier
+costs are unknown here; no consumer cost is priced as zero in a κ calculation.
+This is a structural screen, not an implementation expansion.
+
+Reproduce from the repository root with standard-library Python 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/staggered-single-owner-obstruction
+```
+
+Or copy the package alone and run `python3 -I -B verify.py` and
+`python3 -I -O -B verify.py`. Both print
+`PASS_STAGGERED_SINGLE_OWNER_OBSTRUCTION`. No Git or network is needed by the
+direct verifier. No width-five hook rank engine, Lean, Docker, broad historical
+suite or selected-construction replay is needed or claimed.
+
+## Sources and attribution
+
+- Yiyang (@Lyy-iiis), `phase-prefix-continuations` at
+  `dcd20b2112327d903babbddc654a535dcfdb1b63`: the exact staggered program,
+  two-owner graph screen, uniform-word separation lemma and concrete handoff.
+  Its unchanged `arithmetic.py` is retained here with SHA256
+  `0d277854396e4ceda1e0f26916bd576b6decb474c0692b6671ebf2595283ddb9`
+  (Git blob `9130ce2171e4af01338be27e7ffbf1feaf88da9e`). The new checker adapts
+  its literal row expansion; the source notice is retained alongside it.
+- Yiyang's [PR #4710](https://github.com/CrocSwap/integer-mult-bounds/pull/4710),
+  head `b0d5192390af493d626054b060921895df3c94d2`, supplies the phase-aligned
+  prefix and exact residual identities.
+- lee-phys's [PR #4688](https://github.com/CrocSwap/integer-mult-bounds/pull/4688),
+  head `264c4b3cb13c82d171de352ecf60486dfb8d2bd4`, supplies the two-image
+  construction and hook engine; that expensive engine is not rerun here.
+- Jacob Sussman's [PR #4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628),
+  head `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`, supplies the small-unit
+  model and existing lower bounds, with eumemic/#288 and Swapnil Jain P1/P2
+  as credited there. Those bounds are not rederived.
+
+The source URLs and exact retained bytes provide provenance; none of these
+unmerged commit objects is required at replay. Canonical base is
+`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7, selecting the
+conditional κ 0.00302015. Initial overlap covered 506 open PRs, 3650 Discussion
+records and the complete local-note inventory; it does not cover every closed
+PR or code diff. [Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19130780).
+
+New single-owner witness, proof and checks: JoyboyBrian with substantial
+OpenAI Codex assistance; Apache-2.0. This is author-checked exact evidence,
+not independent human review or a formal-kernel proof.
+
+## Open next questions
+
+1. Change the original x path so its low-order triangular module loses a unit
+   pivot while retaining information. Start with a changed second/fourth call
+   and recompute this six-coset table before expensive hook ranks. A zero pivot
+   only removes this obstruction; it does not construct a target channel.
+2. For any resulting candidate, produce a literal uniform pure-target
+   combination and charge recovery of every independent complement. The
+   present theorem supplies no such candidate and does not justify another
+   search that changes only B or enlarges the projector list.