From 9cf91d3da32e8ed58cc3d3a2962d5963b16067ff Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Fri, 23 Oct 2026 14:07:21 +0100
Subject: [PATCH] feat(research): prove sharp A7+A1 puncture COPY71 floor

---
 research/a7-a1-puncture-optimum/PROOF.md      | 152 ++++++++++++
 research/a7-a1-puncture-optimum/README.md     | 119 +++++++++
 research/a7-a1-puncture-optimum/SOURCES.json  |  30 +++
 research/a7-a1-puncture-optimum/TASK.json     | 104 ++++++++
 research/a7-a1-puncture-optimum/VALIDATION.md |  42 ++++
 research/a7-a1-puncture-optimum/VERIFY.json   |  32 +++
 research/a7-a1-puncture-optimum/verify.py     | 227 ++++++++++++++++++
 7 files changed, 706 insertions(+)
 create mode 100644 research/a7-a1-puncture-optimum/PROOF.md
 create mode 100644 research/a7-a1-puncture-optimum/README.md
 create mode 100644 research/a7-a1-puncture-optimum/SOURCES.json
 create mode 100644 research/a7-a1-puncture-optimum/TASK.json
 create mode 100644 research/a7-a1-puncture-optimum/VALIDATION.md
 create mode 100644 research/a7-a1-puncture-optimum/VERIFY.json
 create mode 100644 research/a7-a1-puncture-optimum/verify.py

diff --git a/research/a7-a1-puncture-optimum/PROOF.md b/research/a7-a1-puncture-optimum/PROOF.md
new file mode 100644
index 0000000000..e214732353
--- /dev/null
+++ b/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.
diff --git a/research/a7-a1-puncture-optimum/README.md b/research/a7-a1-puncture-optimum/README.md
new file mode 100644
index 0000000000..369bdd8008
--- /dev/null
+++ b/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.
diff --git a/research/a7-a1-puncture-optimum/SOURCES.json b/research/a7-a1-puncture-optimum/SOURCES.json
new file mode 100644
index 0000000000..b69ce5c477
--- /dev/null
+++ b/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"
+    }
+  ]
+}
diff --git a/research/a7-a1-puncture-optimum/TASK.json b/research/a7-a1-puncture-optimum/TASK.json
new file mode 100644
index 0000000000..6c06ce5755
--- /dev/null
+++ b/research/a7-a1-puncture-optimum/TASK.json
@@ -0,0 +1,104 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 7,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the exact separate-term COPY minimum for the fixed A7+A1 normals on the E8 P112 coordinate-pair frame puncture, over all independent complex row shifts with zero terms allowed.",
+  "scope_change_reason": "The card asks for a fully paid rank-shape construction. This answers another contributor's explicit puncture question with a sharp algebraic obstruction; no physical supplier is synthesized.",
+  "bottleneck_link": "The sharp bill 71 rules out beating the ordinary P112 separate COPY64 comparator within this fixed punctured normal family. Physical costs remain unknown and are not set to zero.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first verified original optimum; do not extend to other punctures or the all-active optimum.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md and verify.py: complete 43435-plane/304045-annihilator finite lemmas and literal attaining all-pairs identity, plus a written all-complex-shift deficiency bound.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a different frame orbit relative to the fixed A7+A1 normals lower COPY below 71?",
+      "why_it_matters": "A changed puncture can change reader spans and the deficiency restrictions.",
+      "first_step": "Specify one new frame orbit and derive its full reader ranks and conflict-space dimensions.",
+      "blocked_by": "Only the coordinate-pair frame is covered; no replacement finite lemmas or physical bill is supplied."
+    },
+    {
+      "question": "What is the minimum if all nine terms are required active on this puncture?",
+      "why_it_matters": "The present optimum allows a zero term and does not give the active rank-shape bill.",
+      "first_step": "Analyze equality in the deficiency-ten proof and price one exact active witness.",
+      "blocked_by": "The attaining witness here has a zero term; physical consumer costs remain unknown."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146127",
+  "predecessors": [
+    {
+      "pr": 1224,
+      "head": "00e6ed0810b8ebc7f6133e2c036d0f1c9a3a4162",
+      "credit": "joaqcoo; family and row-shift normal form"
+    },
+    {
+      "pr": 2062,
+      "head": "8344a5fc1eb643aca6a21bc745d824a38f449e39",
+      "credit": "Adam Gall; canonical model, unpunctured theorem and puncture question"
+    }
+  ],
+  "overlap": {
+    "checked_at": "2026-10-23T12:58:00Z",
+    "upstream": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+    "open_prs_cached": 341,
+    "discussion_records_cached": 4446,
+    "local_notes_searched": 162,
+    "local_notes_at_head": 6996,
+    "coverage": "Live open/own PR lists, latest 100 handoff comments and active discussions, merged A7/A1/puncture searches and Git-object main README searches supplemented the incomplete sparse-note search. No arbitrary-diff or unpublished-work novelty guarantee."
+  },
+  "orientation": {
+    "selected_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY at the declared base; metadata only.",
+    "historical_card_control": "The requested complex-local-word-ceiling/verify.py was attempted and failed with KeyError: complex_profile because it reads the current selected schema. This historical-control failure is not a mathematical finding. No predecessor result was audited or repaired."
+  }
+}
diff --git a/research/a7-a1-puncture-optimum/VALIDATION.md b/research/a7-a1-puncture-optimum/VALIDATION.md
new file mode 100644
index 0000000000..585e522b05
--- /dev/null
+++ b/research/a7-a1-puncture-optimum/VALIDATION.md
@@ -0,0 +1,42 @@
+# Validation and remaining obligations
+
+Environment: CPython 3.12.15, Clang 23.1.3, macOS arm64; standard library only.
+Interpreter: `/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12`.
+
+Both warning-strict registered checks passed locally. Separately timed
+direct runs took 4.24 seconds normally and 4.20 seconds with `-O`; the
+registered two-command replay took 8.71 seconds including metadata checks.
+These are timeout-budget observations, not comparative performance claims.
+They rebuilt the specified P112 instance and checked the complete
+43,435-plane lemma, 304,045 annihilator comparisons, reverse ranks and the
+COPY71 attainer. Both commands reported
+`PASS_A7_A1_P112_COPY71 planes=43435 annihilator_checks=304045 cost=71`.
+The runner reported `PASS_REGISTERED_RESEARCH_PACKAGE` with
+`outcome=negative-result`. Committed-byte/source-history preflight is run
+against the publication commit before pushing; its output is recorded in
+the PR body.
+
+The current selected metadata orientation returned
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. This is source-bound orientation,
+not an operator replay. The card's historical positive-control command
+`research/complex-local-word-ceiling/verify.py` was also attempted. It failed
+at `asm['complex_profile']` with `KeyError: 'complex_profile'` because that
+historical checker reads the current selected assembly schema. Its source
+was left unchanged. The old ceiling is not a premise of this theorem.
+
+The proof and scientific verifier are self-contained. Source pins preserve
+the catalogue, selected-record context and cited predecessor statements;
+the scientific replay imports no predecessor code. No predecessor theorem
+is offered as newly verified. No handwritten receipt is included.
+
+The new executable uses explicit checks under normal and optimized Python.
+Its mathematical census is finite and complete within the stated binary
+domains. The complex-parameter quantifiers are discharged by the written
+deficiency argument, not by finite complex testing.
+
+Unrun and unclaimed: proof-kernel formalization, independent human proof
+review, the selected construction's cold replay, native and physical
+supplier admission, Lean, Docker, and the complete multiplication theorem.
+Hosted CI is pending at initial publication. There is no all-active optimum
+or statement for other punctures. Acquisition, routing, restoration,
+hosting, stock, precision and recursive-consumer costs remain unpriced.
diff --git a/research/a7-a1-puncture-optimum/VERIFY.json b/research/a7-a1-puncture-optimum/VERIFY.json
new file mode 100644
index 0000000000..d7560280c1
--- /dev/null
+++ b/research/a7-a1-puncture-optimum/VERIFY.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Rebuild punctured geometry, exhaustive binary compatibility and annihilator lemmas, all-pairs attainer, actual invoice, symmetries and semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Repeat complete scientific verification with Python assertions disabled."
+    }
+  ]
+}
diff --git a/research/a7-a1-puncture-optimum/verify.py b/research/a7-a1-puncture-optimum/verify.py
new file mode 100644
index 0000000000..d89b31a7d2
--- /dev/null
+++ b/research/a7-a1-puncture-optimum/verify.py
@@ -0,0 +1,227 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Exact finite lemmas for the specified A7+A1 P112 COPY optimum."""
+
+from collections import Counter
+import hashlib
+from itertools import combinations, product
+import json
+from pathlib import Path
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def basis(rows, width=9):
+    """Internal binary elimination; callers use at most 120 rows."""
+    require(0 < width <= 120 and len(rows) <= 120, "elimination capacity")
+    pivots = [0] * width
+    for row in rows:
+        require(type(row) is int and 0 <= row < 1 << width, "binary row")
+        value = row
+        for column in range(width - 1, -1, -1):
+            if value >> column & 1:
+                if pivots[column]:
+                    value ^= pivots[column]
+                else:
+                    pivots[column] = value
+                    break
+    return tuple(value for value in pivots if value)
+
+
+def dot(left, right):
+    require(len(left) == len(right) <= 9, "dot-product shape")
+    return sum(a * b for a, b in zip(left, right))
+
+
+def roots_and_puncture():
+    roots = set()
+    puncture = set()
+    for i, j in combinations(range(8), 2):
+        for sign in (-2, 2):
+            row = tuple(2 if k == i else sign if k == j else 0 for k in range(8))
+            roots.add(row)
+            if i % 2 == 0 and j == i + 1:
+                puncture.add(row)
+    for row in product((-1, 1), repeat=8):
+        if sum(x < 0 for x in row) % 2 == 0:
+            roots.add(row if row[0] > 0 else tuple(-x for x in row))
+    require(len(roots) == 120 and len(puncture) == 8, "E8 line inventory")
+    deleted = tuple(sorted(puncture))
+    require(all(dot(x, y) == 0 for x, y in combinations(deleted, 2)),
+            "orthogonal puncture")
+    return tuple(sorted(roots - puncture, reverse=True))
+
+
+def model():
+    roots = roots_and_puncture()
+    require(len(roots) == 112 and all(dot(x, x) == 8 for x in roots), "live roots")
+    pairing = tuple(sum(((dot(x, y) // 4 + 1) % 2) << j
+                        for j, y in enumerate(roots)) for x in roots)
+    require(all(dot(x, y) % 4 == 0 for x in roots for y in roots), "integral Gram")
+    require(all(row >> i & 1 for i, row in enumerate(pairing)), "pairing diagonal")
+    row_basis = basis(pairing, 112)
+    require(len(row_basis) == 9, "binary pairing rank")
+    labels = tuple(sum(((row >> i) & 1) << k for k, row in enumerate(row_basis))
+                   for i in range(112))
+    require(len(basis(labels)) == 9 and len(set(labels)) == 112, "faithful labels")
+    words = tuple(sum(((w & label).bit_count() % 2) << i
+                      for i, label in enumerate(labels)) for w in range(512))
+    readers = tuple(tuple(8 * x[k] - sum(x) for k in range(8)) + (4 * sum(x),)
+                    for x in roots)
+    supports = tuple(tuple(i for i in range(112) if readers[i][k]) for k in range(9))
+    require(all(len(basis(tuple(labels[i] for i in support))) == 9
+                for support in supports), "all reader spans have rank nine")
+    fixed = tuple(i for i, x in enumerate(roots) if sum(x))
+    require(len(basis(tuple(labels[i] for i in fixed))) == 9, "forced A1 rank nine")
+    return roots, pairing, labels, words, readers, supports
+
+
+def compatibility(roots, labels, words):
+    tables = []
+    conflicts = []
+    reverse_histograms = []
+    exceptional_labels = []
+    for k in range(1, 8):
+        indices = tuple(i for i, x in enumerate(roots) if x[0] != x[k])
+        mask = sum(1 << i for i in indices)
+        conflicts.append(indices)
+        table = tuple(sum(1 << v for v in range(512)
+                          if words[u] & words[v] & mask == 0) for u in range(512))
+        tables.append(table)
+        ranks = []
+        one_labels = []
+        for z in range(1, 512):
+            space = basis(tuple(labels[i] for i in indices if words[z] >> i & 1))
+            ranks.append(len(space))
+            if len(space) == 1:
+                one_labels.append(space[0])
+        histogram = dict(sorted(Counter(ranks).items()))
+        reverse_histograms.append(histogram)
+        if k == 1:
+            require(histogram == {0: 1, 7: 508, 8: 2}, "paired reverse ranks")
+        else:
+            require(histogram == {1: 1, 7: 254, 8: 255, 9: 1}, "other reverse ranks")
+            root = tuple(2 if j == 0 else -2 if j == k else 0 for j in range(8))
+            expected = labels[roots.index(root)]
+            require(one_labels == [expected], "rank-one space is the named root label")
+            exceptional_labels.append(expected)
+    require(len(basis(tuple(exceptional_labels))) == 6, "six independent exceptions")
+    return tuple(tables), tuple(conflicts), reverse_histograms
+
+
+def plane_lemma(labels, words, tables, conflicts):
+    planes = 0
+    two_dimensional = 0
+    histogram = Counter()
+    for u in range(1, 512):
+        for v in range(u + 1, 512):
+            if v >= u ^ v:
+                continue
+            planes += 1
+            dimensions = []
+            for k in range(7):
+                partner_mask = tables[k][u] & tables[k][v]
+                size = partner_mask.bit_count()
+                require(size > 0 and size & (size - 1) == 0, "partner is a subspace")
+                dimension = size.bit_length() - 1
+                forbidden = words[u] | words[v]
+                rows = tuple(labels[i] for i in conflicts[k] if forbidden >> i & 1)
+                require(dimension == 9 - len(basis(rows)), "independent annihilator check")
+                require(dimension <= (2 if k == 0 else 1), "punctured plane lemma")
+                dimensions.append(dimension)
+            two_dimensional += dimensions[0] == 2
+            histogram[tuple(sorted(dimensions))] += 1
+    require(planes == 43435 and two_dimensional == 254, "complete plane coverage")
+    return {"planes": planes, "annihilator_checks": 7 * planes,
+            "planes_with_paired_dimension_two": two_dimensional,
+            "partner_dimension_histogram": {str(k): v for k, v in sorted(histogram.items())}}
+
+
+def symmetry(roots, pairing, readers):
+    permutations = ((1, 0, 2, 3, 4, 5, 6, 7), (2, 3, 4, 5, 6, 7, 0, 1))
+    for permutation in permutations:
+        transformed = []
+        for row in roots:
+            vector = tuple(row[j] for j in permutation)
+            if next(x for x in vector if x) < 0:
+                vector = tuple(-x for x in vector)
+            transformed.append(roots.index(vector))
+        require(len(set(transformed)) == 112, "puncture symmetry")
+        for i in range(112):
+            for j in range(112):
+                require((pairing[i] >> j & 1) ==
+                        (pairing[transformed[i]] >> transformed[j] & 1), "pairing covariance")
+        require(all(sum(row[:8]) == 0 for row in readers), "eight-way dependency")
+    orbit = {0}
+    for _ in range(8):
+        orbit |= {p[j] for p in permutations for j in tuple(orbit)}
+    require(orbit == set(range(8)), "all anchor columns covered")
+
+
+def endpoint(roots, readers, shifts, keep_a1=True):
+    """Shifts are exact Gaussian-integer pairs; matrices are scaled by four."""
+    require(len(shifts) == 112, "one shift per live line")
+    for i, x in enumerate(roots):
+        real, imaginary = shifts[i]
+        d4 = tuple(4 * (x[k] + real) for k in range(8)) + ((sum(x) if keep_a1 else 0),)
+        for j, y in enumerate(roots):
+            if dot(d4, readers[j]) != 32 * dot(x, y):
+                return False
+            if imaginary * sum(readers[j][:8]) != 0:
+                return False
+    return True
+
+
+def witnesses_and_controls(roots, pairing, labels, readers, supports, tables):
+    shifts = tuple((-row[0], 0) for row in roots)
+    require(endpoint(roots, readers, shifts), "rational attaining all-pairs identity")
+    row_supports = tuple(tuple(i for i, x in enumerate(roots)
+                              if (x[k] != x[0] if k < 8 else sum(x) != 0))
+                         for k in range(9))
+    ranks = []
+    for k in range(9):
+        mask = sum(1 << i for i in supports[k])
+        actual = len(basis(tuple(pairing[i] & mask for i in row_supports[k]), 112))
+        require(actual == len(basis(tuple(labels[i] for i in row_supports[k]))),
+                "actual support-pair rank agrees with label rank")
+        ranks.append(actual)
+    require(ranks == [0, 8, 9, 9, 9, 9, 9, 9, 9] and sum(ranks) == 71, "sharp COPY71")
+    require(not endpoint(roots, readers, shifts, keep_a1=False), "missing A1 rejected")
+    d4 = tuple(4 * (x - roots[0][0]) for x in roots[0]) + (sum(roots[0]),)
+    corrupted = (d4[0] + 1,) + d4[1:]
+    require(any(dot(corrupted, readers[j]) != 32 * dot(roots[0], y)
+                for j, y in enumerate(roots)), "one bad coefficient rejected")
+    changed = ((shifts[0][0] + 1, 0),) + shifts[1:]
+    require(endpoint(roots, readers, changed), "independent row shift remains legal")
+    generic = tuple((0, 1) for _ in roots)
+    require(endpoint(roots, readers, generic), "genuinely complex shifts")
+    require(any((tables[0][u] & tables[0][v]).bit_count() == 4
+                for u in range(1, 512) for v in range(u + 1, 512) if v < u ^ v),
+            "dimension-one transfer fails after puncturing")
+    return {"minimum_copy": 71, "attaining_ranks": ranks,
+            "all_pairs_per_successful_endpoint": 112 * 112,
+            "successful_endpoint_fixtures": 3,
+            "control_names": ["deleted A1", "corrupted coefficient", "false dimension-one lemma",
+                              "valid changed row", "nonreal shifts"]}
+
+
+def main():
+    roots, pairing, labels, words, readers, supports = model()
+    symmetry(roots, pairing, readers)
+    tables, conflicts, reverse_histograms = compatibility(roots, labels, words)
+    result = plane_lemma(labels, words, tables, conflicts)
+    result.update(witnesses_and_controls(roots, pairing, labels, readers, supports, tables))
+    result["reverse_rank_histograms"] = reverse_histograms
+    here = Path(__file__).resolve().parent
+    files = tuple(sorted(path for path in here.iterdir() if path.is_file()))
+    require(len(files) <= 8, "package file capacity")
+    result["sha256"] = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() for path in files}
+    print(json.dumps(result, sort_keys=True))
+    print("PASS_A7_A1_P112_COPY71 planes=43435 annihilator_checks=304045 cost=71")
+
+
+if __name__ == "__main__":
+    main()