Prove sharp COPY71 for the coordinate-frame A7+A1 puncture

research/a7-a1-puncture-optimum/PROOF.md

@@ -0,0 +1,152 @@
+# The coordinate-frame puncture has exact COPY cost 71
+
+This is a scoped proof with exhaustive finite binary lemmas. All row-shift
+parameters are arbitrary complex numbers. Zero terms are allowed. The theorem
+concerns this fixed normal family and this fixed puncture only.
+
+## Model and exact row solutions
+
+Take the 120 unoriented E8 root lines represented by
+`e_i +/- e_j` and half-sign vectors with an even number of minus signs.
+Choose the representative whose first nonzero entry is positive. Remove
+
+```text
+e0 +/- e1, e2 +/- e3, e4 +/- e5, e6 +/- e7.
+```
+
+These eight lines are an orthogonal frame. Write the remaining doubled roots
+as `x_i=2r_i`, so `x_i.x_i=8`. The nine fixed reader normals are
+
+```text
+b_k = e_k - (1/8)1, k=0,...,7;       a=(1/2)1.
+```
+
+These are the canonical A7+A1 normals of Adam Gall's
+[PR2062](https://github.com/CrocSwap/integer-mult-bounds/pull/2062), which
+binds them to joaqcoo's [PR1224](https://github.com/CrocSwap/integer-mult-bounds/pull/1224).
+That source identification is cited predecessor work, not a replay claim.
+
+Put `T_ik=<r_i,b_k>` and `T_i8=<r_i,a>`. The all-pairs identity is
+`D T^transpose = 2G`, with `G_ij=<r_i,r_j>` and ordinary transpose. The live
+roots span eight-space. Since the only normal dependency is `sum b_k=0`,
+the complete row solution is
+
+```text
+D_ik = x_ik + t_i, k<8;       D_i8 = sum_k x_ik / 4;       t_i in C.
+```
+
+For completeness, subtracting the mean of `x_i` in the eight `b_k` terms
+and adding the displayed A1 term gives exactly `x_i=2r_i`. Conversely,
+equality against every live root forces that vector equation. Its kernel
+is exactly the stated one-dimensional dependency. The remaining D8 roots
+alone span eight-space: for each coordinate, choose a coordinate in another
+pair and add/subtract the two retained signed roots.
+
+Define the binary pairing `B_ij=(G_ij+1) mod 2`. For actual nonzero row and
+reader supports `X_k,Y_k`, the separate-term bill is
+
+```text
+COPY(D) = sum_(k=0)^8 rank_F2 B[X_k,Y_k].
+```
+
+No simultaneous or shared physical-copy discount is included.
+
+## New finite lemmas after puncturing
+
+The standalone checker rebuilds the punctured geometry. Its pairing has
+rank nine. Choose a basis of its row space and let `l_i in F2^9` be its
+evaluation column at root i. All nine reader supports span the label space;
+the fixed A1 row support also spans it. Thus the A1 term costs nine.
+
+Because B is symmetric of rank nine, it has a factorization
+`B=L Omega L^transpose`, where the rows of L are the labels and Omega is
+invertible. A reader support of full label rank makes
+`rank B[X,Y] = dim span{l_i:i in X}`. This justifies using label ranks for
+each term. The attaining witness is additionally priced by literal pairing
+submatrices, independently of this shortcut.
+
+For a character w write `s(w)={i:w.l_i=1}`. For k=1,...,7 let
+
+```text
+C_k = {i:x_i0 != x_ik},
+F_k(z) = span{l_i:i in C_k intersect s(z)},
+H_k(U) = {z:s(z) intersect C_k intersect union_(u in U)s(u) is empty}.
+```
+
+H_k(U) is a binary annihilator space. If `U=<u,v>`, the union of character
+supports is `s(u) union s(v)`. The checker enumerates every binary plane
+exactly once using `0<u<v<u xor v`, and verifies:
+
+1. On all 43,435 planes U, `dim H_1(U)<=2`, and `dim H_k(U)<=1` for k=2,...,7.
+2. Among all 511 nonzero z, `rank F_1(z)` has histogram
+   `{0:1,7:508,8:2}`.
+3. For each k=2,...,7 the corresponding histogram is
+   `{1:1,7:254,8:255,9:1}`. The unique rank-one case is exactly the span of
+   `q_k=l_(e0-e_k)`.
+4. The six labels q_2,...,q_7 are independent.
+
+The plane enumeration performs 304,045 comparisons between two descriptions
+of H: intersection of complete character compatibility masks, and direct
+binary elimination of the forbidden labels. It finds 254 planes with
+`dim H_1(U)=2`. Therefore the old P120 dimension-one premise cannot simply
+be transferred to this puncture. The seven reverse-rank histograms enumerate
+all nonzero characters, not sampled coefficients or subspaces.
+
+Coordinate pair rotations and swaps within a pair preserve the puncture,
+the normal family, and the binary pairing. They act transitively on the eight
+mutable columns. The checker verifies generating symmetries. Consequently
+any chosen mutable column may be the anchor called zero, with its paired
+coordinate called one.
+
+## Uniform deficiency bound
+
+For each mutable term let K_k be the characters annihilating its actual row
+support and put `delta_k=dim K_k`. The total bill is
+
+```text
+COPY(D) = 81 - sum_(k=0)^7 delta_k.
+```
+
+If `u in K_0` and `z in K_k`, a root in both character supports forces
+`D_i0=D_ik=0`, hence `x_i0=x_ik`. Thus `K_k subset H_k(U)` whenever
+`U subset K_0`, and `K_0 subset F_k(z)^perp` for every `z in K_k`.
+These implications use exact zero equalities and hold over C without any
+finite restriction on the t_i.
+
+If every delta is at most one, their sum is at most eight. Otherwise use the
+puncture symmetry to choose an anchor with `delta_0>=2`, and choose a plane
+in K_0. Lemma 1 bounds `delta_1<=2` and every other delta by one.
+If `delta_0=2`, the sum is at most `2+2+6=10`.
+
+Suppose instead `delta_0>=3`. For every nonzero `z in K_k`, containment in
+`F_k(z)^perp` implies `rank F_k(z)<=6`. Lemma 2 permits only one nonzero
+character in K_1, so `delta_1<=1`. For k>=2, Lemma 3 permits only the unique
+rank-one exception. Let J be the set of such k with K_k nonzero. Each has
+delta one and forces K_0 to annihilate q_k. Lemma 4 gives |J| independent
+conditions, so
+
+```text
+delta_0 <= 9-|J|,
+sum delta_k <= (9-|J|) + 1 + |J| = 10.
+```
+
+This exhausts all cases. Therefore every complex-shift decoder in this
+family has `COPY(D)>=71`.
+
+## Attainment and consequence
+
+Set `t_i=-x_i0` on every live line. The actual support-pair ranks are
+
+```text
+(0,8,9,9,9,9,9,9,9),      total 71.
+```
+
+The checker verifies all 12,544 all-pairs equations and prices all nine
+support submatrices. Thus 71 is the exact minimum, with zero terms allowed.
+This theorem does not determine the optimum with every term active.
+
+The result answers this specified-puncture branch of PR2062's first open
+question. It also excludes beating the ordinary P112 separate COPY bill
+64 through these normals and this puncture. It is an algebraic obstruction
+for the declared billing model. No physical supplier, full recursive moment,
+new kappa, or complete multiplication theorem follows.

research/a7-a1-puncture-optimum/README.md

@@ -0,0 +1,119 @@
+# Sharp COPY71 for the coordinate-frame A7+A1 puncture
+
+For the fixed A7 weights plus A1 normal family, remove the eight E8 lines
+`e0 +/- e1, e2 +/- e3, e4 +/- e5, e6 +/- e7`. The exact separate-term COPY
+minimum on the remaining 112 lines is **71**, allowing arbitrary independent
+complex row shifts and allowing zero terms. The rational witness has ranks
+`(0,8,9,9,9,9,9,9,9)`.
+
+This is a scoped written proof with exhaustive finite binary lemmas. It
+answers the specified-puncture question in Adam Gall's
+[PR2062](https://github.com/CrocSwap/integer-mult-bounds/pull/2062), whose
+P120 optimum is cited, not replayed. The COPY71 floor excludes beating the
+ordinary P112 COPY64 comparator with these normals and this puncture.
+No supplier, full recursive moment, new kappa or selected-frontier change
+is claimed.
+
+## Proof and evidence
+
+[PROOF.md](PROOF.md) gives the complete complex-parameter argument. The
+puncture creates a two-dimensional partner space in 254 binary-plane cases,
+so the old dimension-one argument cannot be transferred. New finite lemmas
+bound the total row-support deficiency by ten, giving `81-10=71`.
+
+The standalone standard-library verifier constructs the roots and puncture
+directly. It imports no predecessor code and runs no predecessor verifier.
+Its complete finite evidence includes:
+
+- All 43,435 planes in the nine-dimensional binary character space, with
+  304,045 comparisons of compatibility-mask and direct-annihilator calculations.
+- All 511 nonzero characters for each of seven conflict sets, including
+  the six independent exceptional root labels used by the proof.
+- The puncture-preserving symmetries needed to cover all eight anchor columns.
+- All 12,544 equations for each of three successful endpoint fixtures,
+  including a genuinely nonreal shift. The attaining invoice is computed
+  directly from the actual binary support-pair submatrices.
+- Rejection of a deleted A1 term and a single corrupted coefficient, and
+  a discriminator showing that the old dimension-one premise fails here.
+
+The universal complex-shift statement uses the written deficiency proof;
+it is not inferred from a sample of scalar parameters. No receipt is
+handwritten or committed. Each run emits its computed evidence and SHA256
+hashes of the package's regular files to stdout.
+
+## Reproduce
+
+From the worktree root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a7-a1-puncture-optimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/a7-a1-puncture-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/a7-a1-puncture-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a7-a1-puncture-optimum --check-source-history
+```
+
+Another CPython 3.12 installation can replace the absolute interpreter path.
+Expected scientific marker:
+
+```text
+PASS_A7_A1_P112_COPY71 planes=43435 annihilator_checks=304045 cost=71
+```
+
+Both registered commands have 120-second limits. Default replay writes no
+files. [VALIDATION.md](VALIDATION.md) records actual local results and limits.
+
+## Scope and implementation constraints
+
+The theorem fixes the normals, puncture, all-pairs identity and additive
+separate-term pairing-rank charge. The all-nine-active optimum, other
+punctures, shared copies and masked identities are outside scope. Native
+acquisition, delivery, restoration, frames, hosting, precision and compiler
+costs remain unpriced. No selected cold replay, Lean or Docker build was run.
+Independent human and formal proof-kernel review are unclaimed.
+
+The verifier has no recursion, dynamic imports, subprocesses or network
+calls. All functions fit within 60 physical lines. Loops are bounded by 120
+root lines, 512 characters, seven conflict sets, 43,435 planes, nine matrix
+columns or eight symmetry steps. Binary elimination accepts at most 120
+rows and 120 columns. The plane search visits at most `512^2` candidate
+character pairs. Checks use explicit exceptions and remain active
+under optimization.
+
+Power of Ten rule 3 deviation: CPython allocates managed objects during the
+finite calculation. The largest retained compatibility table contains
+`7*512` integers of at most 512 bits; live root and matrix collections have
+at most 120 entries per axis. Temporary forbidden-label tuples have at most
+112 entries and are discarded after each calculation. A fixed-allocation
+rewrite would require a different runtime. Review these bounds before
+allowing variable geometries. Warning-strict normal and optimized runs
+provide the available Python diagnostics; no additional static analyzer
+or repository-wide configuration change is introduced.
+
+## Open next questions
+
+- Can a frame puncture in a different orbit relative to these A7+A1 normals
+  lower COPY below 71? Start by deriving its reader ranks and conflict-space
+  dimensions. This result covers only the coordinate-pair frame; changed
+  partner dimensions block reusing the proof without new lemmas.
+- What is the optimum for this puncture if all nine terms must be active?
+  Start with equality in the deficiency-ten bound and price an exact active
+  witness. The present attainer has one zero term, so no active optimum is
+  supplied. Its physical relevance still needs a fully paid consumer.
+
+## Sources and credit
+
+This contribution was produced by Nick Petalas. New work is Apache-2.0.
+Credit joaqcoo [#1224](https://github.com/CrocSwap/integer-mult-bounds/pull/1224)
+for the family and complete row-shift normal form; Adam Gall
+[#2062](https://github.com/CrocSwap/integer-mult-bounds/pull/2062), head
+`8344a5fc1eb643aca6a21bc745d824a38f449e39`, for the canonical model,
+unpunctured theorem and explicit puncture question; Philipp / mightyOil
+[#1248](https://github.com/CrocSwap/integer-mult-bounds/pull/1248) for the
+deficiency-space method; DreamingOfClouds #446/#595/#717 for the decoder
+and separate COPY model; and the retained E8 geometry lineage.
+
+Canonical base is `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority
+revision 7. [SOURCES.json](SOURCES.json) pins predecessor/context prose;
+none is executable input. [TASK.json](TASK.json) records the changed card
+scope and overlap coverage. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146127)
+preceded the new finite computation. Frozen predecessor packages are unchanged.

research/a7-a1-puncture-optimum/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/a7-a1-decoder-floor/README.md",
+      "usage": "provenance",
+      "git_blob": "c6f3649af2bb2d91f10127b89eabb3a3c007f166",
+      "sha256": "b05e08146efb393415aad940a7cb4566fa63a9e37138e06ff8e9ea06e04cd476"
+    },
+    {
+      "path": "research/nine-term-decoder-normal-form-seed42/README.md",
+      "usage": "provenance",
+      "git_blob": "9cf8ecd3eda302b57ab14302c429b00c255f2dba",
+      "sha256": "d272081da47d6ea6a2404fddff211418dd6e7c236babf7eb4560737e818c1677"
+    }
+  ]
+}