Research: sharp A8 simplex P112 copy floor 71 on matching-frame punctures (no new kappa)

research/a8-p112-decoder-screen/PROOF.md

@@ -0,0 +1,185 @@
+# Sharp copy cost 71 for the A8 simplex on a matching-frame P112 puncture
+
+This is a scoped mathematical proof whose finite lemmas are exhaustively
+recomputed by two implementations. It is not a formal multiplication theorem.
+The deficiency-space method is due to the P120 predecessor, mightyOil's
+[PR1248](https://github.com/CrocSwap/integer-mult-bounds/pull/1248). The one-sided
+overcomplete representation comes from joaqcoo's
+[PR1224](https://github.com/CrocSwap/integer-mult-bounds/pull/1224). Here the
+puncture changes the finite lemmas, and every lemma needed below is recomputed.
+
+## 1. Fixed family and puncture
+
+Work in the sum-zero subspace V of Q^9. Use the 120 oriented E8 root lines
+
+- e_a-e_b for 0 <= a < b <= 8, in lexicographic order (36 lines);
+- 1_S-(1/3)1 for three-element subsets S of {0,...,8}, in lexicographic order
+  (84 lines).
+
+Puncture the orthogonal frame
+
+    F = { e_(2j)-e_(2j+1),
+          e_(2j)+e_(2j+1)+e_8-(1/3)1 : j=0,1,2,3 }.
+
+Its zero-based indices are [0,15,26,33,42,89,112,119]. It is the first
+orthogonal eight-frame in the declared root order; the verifier checks this
+by complete lexicographic backtracking until the first solution. Let P be
+the 112 live lines. They span V (rank eight, checked over Q).
+
+Fix the nine simplex normals b_k=e_k-(1/9)1, and T_ik=r_ik for live roots r_i.
+The variable factor D has 112 rows and nine columns. Require
+
+    D T^t = 2G,   G_ij = r_i dot r_j,
+
+on **all** live pairs, with ordinary transpose. Coefficients can be arbitrary
+complex numbers. Terms are charged separately by the F2 rank of the pairing
+matrix (G_ij+1) mod 2 restricted to their nonzero row and column supports.
+Zero terms are allowed, but the sharp witness below has all nine terms active.
+
+Since the live roots span V, the identity is equivalent to
+
+    D_ik = 2r_ik + t_i,   t_i arbitrary in C.
+
+Indeed D_i-2r_i is orthogonal to V and hence is a multiple of the all-ones
+vector. This argument is valid over C with the bilinear ordinary transpose;
+no positivity or conjugation is invoked.
+
+## 2. Exact reduction to binary deficiency spaces
+
+Use labels in F2^9:
+
+    u_ab = 1+e_a+e_b,    u_S = 1_S.
+
+For every pair of the 120 roots, u_i dot u_j=(G_ij+1) mod 2. This is checked
+on all 14,400 entries. For each k, the live labels on the column support
+{i:r_ik != 0} span all of F2^9. Thus the pairing rank of term k equals the
+dimension of the label span on its row support {i:D_ik != 0}.
+
+Define
+
+    K_k = {w : w dot u_i=0 whenever D_ik != 0},   delta_k=dim K_k.
+
+The total copy cost is exactly 81-sum_k delta_k. It is enough to prove that
+the sum of the nine deficiencies is at most ten.
+
+If w in K_j and z in K_k both evaluate to one on u_i, then D_ij=D_ik=0.
+Consequently r_ij=r_ik. Call this necessary relation compatibility of the two
+functionals at columns j,k. It uses only zero patterns, so it applies to all
+complex shifts, including generic shifts that create no zero entries.
+
+## 3. Finite covering of every possible deficiency tuple
+
+If every delta_k <= 1, the sum is at most nine already. Otherwise choose an
+anchor j with delta_j >= 2 and a binary plane U contained in K_j. We check
+every anchor and every plane; no symmetry assumption enters the primary check.
+
+Each binary plane has a unique representation by 0<a<b<a xor b. There are
+511*510/6=43,435 planes. For each k != j, let H_k(U) consist of the functionals
+z compatible with both basis vectors of U. Compatibility with a basis is
+equivalent to compatibility with all of U: an evaluation of a linear
+combination can be nonzero only if some basis evaluation is nonzero. Hence
+
+    K_k subset H_k(U).
+
+H_k(U) is a subspace, being the annihilator of the labels u_i for which
+r_ij != r_ik and some member of U evaluates nontrivially. The complete census
+checks dim H_k <= 2. Unlike P120, dimension two really occurs: at anchor 0,
+U=span(1,508), H_1 has dimension two. The P120 dimension-one lemma cannot be
+reused here.
+
+Every subspace L_k of H_k is enumerated: zero, every one-dimensional subspace,
+and the whole plane if H_k has dimension two. For a choice (L_k)_(k != j):
+
+1. Reject it if some pair L_k,L_l is incompatible. Checking unions of the
+   nonzero evaluation supports of basis vectors checks all elements of each
+   subspace, by the same linearity observation.
+2. Form Q as the span of labels u_i such that, for some k != j, r_ij != r_ik
+   and some z in L_k evaluates nontrivially on u_i.
+3. Compatibility with K_j implies K_j subset Q^perp. Therefore this tuple has
+   the upper bound
+
+       sum_k delta_k <= 9 - dim Q + sum_(k != j) dim L_k.
+
+The actual tuple L_k=K_k appears in this enumeration, survives the necessary
+compatibility tests, and satisfies this upper bound. The enumeration need not
+assert that every surviving relaxed tuple is realized by a decoder.
+
+Planes with identical ordered partner spaces are grouped only to avoid
+rechecking the identical subspace product. Q and the product depend solely on
+those spaces and the anchor. The complete plane-to-space census is still
+performed, and multiplicities total 43,435 at each anchor.
+
+## 4. Exhaustive lemma and conclusion
+
+The exact results are:
+
+| Anchor | Planes | Distinct ordered partner-space tuples | Compatible subspace choices | Largest upper bound |
+|---|---:|---:|---:|---:|
+| Each of 0,...,7 | 43,435 | 2,131 | 52,832 | 10 |
+| 8 | 43,435 | 2,251 | 39,485 | 9 |
+| Total | 390,915 | 19,299 | 462,141 | 10 |
+
+Thus every possible deficiency tuple has sum at most ten, and **copy cost is
+at least 71**. The census is over a finite covering of the zero-pattern
+constraints, not over a finite set of sampled complex coefficients.
+
+`verify.py` recomputes the complete table and partner-dimension histograms,
+compares every receipt field with `CERTIFICATE.json`, and verifies the model
+and witness identities. The separate `independent.py` derives binary labels
+from independent columns of the Gram pairing matrix, obtains partner spaces
+by row reduction and annihilators, and enumerates Cartesian products without
+the primary's incremental compatibility pruning. It tests compatibility by
+requiring equal forced coefficient values at each live row. It checks two
+anchor representatives and explicitly verifies four puncture-stabilizing
+coordinate permutations whose orbits are {0,...,7} and {8}. Its aggregate
+counts and upper bounds agree with the primary's nine-anchor census.
+
+Mutual compatibility matters. For anchor 0 and U=span(1,508), dropping it
+allows upper bound 11 (the apparent price 70); retaining it gives ten.
+This is a failed necessary-condition relaxation, not a price-70 decoder.
+
+## 5. Sharp witness, including nine active terms
+
+Initially set t_i=-2r_i0. Column 0 is zero and the term costs are
+
+    (0,8,9,9,9,9,9,9,9).
+
+For the single live root r=e_0-e_2, change its shift to t_i=-2r_i2. This
+preserves the all-pairs identity and makes every term active, with costs
+
+    (1,8,8,9,9,9,9,9,9), total 71.
+
+The primary checks all 12,544 identity entries for each witness using integer
+denominator clearing. The separate checker uses rational coefficients and
+computes the term costs from the actual binary pairing submatrices, without
+the full-column-rank shortcut. The optimum is therefore exactly 71 whether
+zero terms are allowed or all nine terms must be active.
+
+## 6. Coordinate-permutation corollary and scope
+
+The fixed simplex family is invariant under all nine-coordinate permutations:
+they permute its columns and root lines, with possible sign changes of the
+chosen pair-root representatives. These signs preserve supports and the
+all-pairs equation after applying the corresponding row signs to D and T.
+The pairing is also unchanged modulo two. Hence the same sharp floor holds
+for every coordinate-permutation image of F.
+
+These are precisely the frames obtained by choosing a singleton coordinate
+and a perfect matching of the other eight coordinates, then taking one pair
+root and one triple root (the pair plus the singleton) for each matched pair.
+There are 9 * 8!/(2^4*4!) = **945 distinct frames**. The four pair-root lines
+identify the matching and the singleton, so no two choices coincide.
+The verifier constructs all 945 and checks their orthogonality. No claim is
+made for frame punctures outside this orbit or for a different simplex family.
+
+The ratio 71/112 exceeds 64/112. This rules out a copied-information saving
+for this family before paying any additional realization costs. It is not a
+complete moment invoice or a lower bound for multiplication. Other normals,
+other punctures, masked identities, two unrestricted factors, shared-copy
+billing and physically different operation contracts remain outside scope.
+All selected-supplier all-size/compiler, common-label/mutable-source, hosting,
+precision/tape, recovery, analytic-transfer and bit-interface obligations
+remain untouched.
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+Apache-2.0. No independent human review or Lean proof is claimed.

research/a8-p112-decoder-screen/README.md

@@ -0,0 +1,129 @@
+# A8 simplex P112 decoder: sharp copy cost 71 on matching-frame punctures
+
+**Scoped proof with exhaustive finite lemmas; no new kappa or physical supplier.**
+For the fixed A8 simplex nine-term all-pairs decoder, removing the specified
+orthogonal eight-frame gives exact minimum copy cost **71**, even with arbitrary
+complex per-root shifts. A witness with all nine terms active has term costs
+`(1,8,8,9,9,9,9,9,9)`. Coordinate permutations extend the result to the **945
+matching-frame punctures** in this orbit. Other frame orbits are unclaimed.
+
+[PR1248](https://github.com/CrocSwap/integer-mult-bounds/pull/1248) proved the
+fixed-simplex P120 floor 72 and explicitly left a P112 frame puncture as its
+first open question. This package answers that question for one orbit. Since
+`71/112 > 64/112`, the family cannot improve the standard P112 copied-information
+bill, even before extra physical costs. This is a copy-cost rejection of one
+route, not a completed recurrence calculation or a bound for arbitrary decoders.
+
+## Exact scope and evidence
+
+The roots are `e_a-e_b` and `1_S-(1/3)1` in the sum-zero subspace of Q^9. The
+fixed column normals are `b_k=e_k-(1/9)1`. On live roots, `T_ik=r_ik` and every
+exact decoder is `D_ik=2r_ik+t_i`, with arbitrary `t_i` in C and ordinary
+transpose. The puncture is
+
+```text
+F = {e_(2j)-e_(2j+1), e_(2j)+e_(2j+1)+e_8-(1/3)1 : j=0,1,2,3}
+```
+
+It has indices `[0,15,26,33,42,89,112,119]` in the pair-then-triple lexicographic
+root order. Terms are billed separately by binary pairing rank. Masked
+identities and shared-copy pricing are excluded.
+
+All nine column-label spans still have rank nine, so the copy cost is
+`81 - sum(delta_k)`. However, puncturing creates two-dimensional partner
+deficiency spaces: the P120 dimension-one lemma is false here. Enumerating all
+subspaces of these enlarged spaces and imposing their mutual compatibility
+proves `sum(delta_k) <= 10`.
+
+- Primary replay: all nine anchors, 390,915 binary planes, 19,299 distinct
+  ordered partner-space tuples, and 462,141 compatible subspace choices.
+- Separate replay: labels reconstructed from the Gram pairing matrix,
+  annihilator row reduction, direct Cartesian-product enumeration, and a
+  checked stabilizer transporting two anchor representatives to all nine.
+- Both check all 12,544 entries of the active witness. The primary also checks
+  the zero-term witness; the separate checker prices actual pairing submatrices.
+- Eight semantic controls include a coefficient error, a deleted term, corrupt
+  labels, a nonorthogonal puncture, the false inherited dimension-one lemma,
+  missing mutual compatibility, a false cost of 70, and a valid non-real shift.
+- Six package tests exercise optimized relocated/read-only replay, the separate
+  checker without the primary file, and changed, incomplete, missing or
+  malformed receipts.
+
+The argument covering every complex shift is in [PROOF.md](PROOF.md). The
+deterministic finite evidence is [CERTIFICATE.json](CERTIFICATE.json). The
+second implementation is by the same AI assistant, not independent human review.
+
+## Reproduce
+
+From the repository root, Python 3.12 and the standard library:
+
+```sh
+python3 -I -B research/a8-p112-decoder-screen/verify.py
+python3 -I -B research/a8-p112-decoder-screen/independent.py
+python3 scripts/research_package.py --package research/a8-p112-decoder-screen --check-only
+python3 scripts/research_package.py --package research/a8-p112-decoder-screen
+```
+
+The last command runs both checkers and the six package tests. Expected markers:
+
+```text
+PASS_A8_P112_DECODER_FLOOR planes=390915 configurations=19299 compatible_leaves=462141 cost=71 controls=8
+PASS_A8_P112_INDEPENDENT anchors=2 transported=9 planes=86870 compatible_leaves=92317 cost=71
+PASS_REGISTERED_RESEARCH_PACKAGE research/a8-p112-decoder-screen outcome=negative-result
+```
+
+`verify.py --write` explicitly regenerates the certificate. Normal replay is
+read-only. Source pins and exact predecessor heads are in [SOURCES.json](SOURCES.json);
+the pending predecessors are attribution/context, not imported code or assumed
+finite lemmas. [TASK.json](TASK.json) records the chooser, scope and next questions.
+See [VALIDATION.md](VALIDATION.md) for measured checks and limits.
+
+No supplier word, delivery/frame/restoration/hosting invoice, new moment,
+selected cold replay, Lean proof, or complete multiplication theorem is supplied.
+The selected frontier and all inherited all-size/compiler, common-label and
+mutable-source, hosting, precision/tape, recovery, analytic-transfer and bit
+H1-H5 obligations remain unchanged. Hosted CI and human review are unclaimed.
+
+## Coordination
+
+Base `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`; chooser nonce
+`a57142e8e77d6c0af036ca35809daf69`, track `complex-mechanisms`, revision 2,
+card `complex-masked-decoder`, scope key `2a6f2c726b78f9ae7d26`. This refines
+the card's overcomplete-family branch to PR1248's explicit puncture question.
+
+Nearest predecessors are PR1248 (P120 optimum) and PR1224 (normal form and
+bounded searches). PR1212/1213 and discussion #1275 concern eight-term masked
+rigidity; PR1236 and discussion #1267 concern masked root-star/co-star supports.
+These are distinct hypotheses. Two parallel sessions from the same account
+study bit-side zero-frame feedback (discussion #1290) and selected bit hosting
+(discussion #1289); this package does neither. The original claim is in
+[discussion #1241](https://github.com/CrocSwap/integer-mult-bounds/discussions/1241#discussioncomment-18909913).
+The final overlap check used a shared snapshot of 788 open PRs and 40
+discussion records with complete pagination, fetched at 21:54:03 and 21:54:12
+UTC on 2026-10-13. It may miss later changes.
+
+## Open next questions
+
+- **Other frame punctures relative to the fixed simplex.** Do they also have
+  minimum cost at least 64? Enumerate orthogonal frames and their S9 orbits,
+  then recompute column ranks and partner dimensions for a representative
+  outside the matching-frame orbit. This tests whether the remaining P112
+  part of PR1248's question can improve copy cost. The present enumerator
+  deliberately rejects partner dimensions above two and may need extension.
+- **Another specified nine-normal frame.** Can the A7+A1 or A2+E6 family in
+  PR1224 admit copy cost below 64 on a named P112 puncture? First establish its
+  exact ratio classes, column spans and a favorable complete cost budget.
+  The simplex's common kernel vector and compatibility census do not transfer
+  automatically; physical realization would remain an additional obligation.
+
+## Credit and disclosure
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+
+Credit Philipp / **mightyOil**, PR1248, for the deficiency-space method, P120
+floor and explicit P112 follow-up; **joaqcoo**, PR1224, for the nine-term normal
+form, A8 frame and ratio-class viewpoint; **DreamingOfClouds**, PR717/595/446,
+for the decoder and pairing-rank cost model; **themilkman216**, PR968, and
+**woklerx**, PR1077/1180, for surrounding floor results; and the classical
+E8/A8 geometry. The selected supplier lineage retains its existing credit.
+No predecessor file is changed. New work is Apache-2.0, the repository license.

research/a8-p112-decoder-screen/SOURCES.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    },
+    {
+      "path": "research/complex-decoder-field-extension-seed44/README.md",
+      "usage": "input",
+      "git_blob": "a6e6d2e04249191c1bce5c6e2977c11f9969b7a3",
+      "sha256": "788a99eef3f187c2cbff6d490933fcc8f8e7fd15d1b685c188023605916887d4"
+    },
+    {
+      "path": "research/complex-frame-pair-decoders/README.md",
+      "usage": "input",
+      "git_blob": "be5bbbee8e30a4ee39fa513896e8fc7e0bb3721e",
+      "sha256": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e"
+    }
+  ],
+  "predecessor_references": [
+    {
+      "pr": 1248,
+      "head": "f226f4329a996b0a1bea8794179a91b5d0ed80bf",
+      "author": "Philipp / mightyOil",
+      "role": "Method and question attribution; no imported code or unverified finite-lemma dependency. Not required for runtime replay.",
+      "files": [
+        {
+          "path": "research/a8-simplex-decoder-floor/README.md",
+          "git_blob": "cc814ae890f18da884b70ae6e471f31a75bade5f",
+          "sha256": "4f279ea113cea46593609cdcd580099c24ec8aa02428aae0c5bae54baa0e4557"
+        },
+        {
+          "path": "research/a8-simplex-decoder-floor/PROOF.md",
+          "git_blob": "4d1d3bcd8799c833dfbb63ed5319af5fe863fa1a",
+          "sha256": "7e3a5407fc535fd9cc7f25f06aab787b0216f09121e571938cccedb383aab3c4"
+        }
+      ]
+    },
+    {
+      "pr": 1224,
+      "head": "00e6ed0810b8ebc7f6133e2c036d0f1c9a3a4162",
+      "author": "joaqcoo",
+      "role": "Method and question attribution; no imported code or unverified finite-lemma dependency. Not required for runtime replay.",
+      "files": [
+        {
+          "path": "research/nine-term-decoder-normal-form-seed42/README.md",
+          "git_blob": "9cf8ecd3eda302b57ab14302c429b00c255f2dba",
+          "sha256": "d272081da47d6ea6a2404fddff211418dd6e7c236babf7eb4560737e818c1677"
+        },
+        {
+          "path": "research/nine-term-decoder-normal-form-seed42/PROOF.md",
+          "git_blob": "e510fd180a286445fd6fc484057001bfc60f8c9c",
+          "sha256": "0503e07f1764708e9e72c01be88d3dad1b213e73eb3c23397a603032791fd23a"
+        }
+      ]
+    }
+  ]
+}