Research: sharp COPY71 on the remaining A8 simplex P112 frame orbit (no new kappa)

research/a8-one-pair-frame-floor/PROOF.md

@@ -0,0 +1,174 @@
+# The complementary A8 simplex frame orbit
+
+This proof follows PR1248's deficiency method and PR1304's punctured-frame
+extension. The changed frame, orbit coverage and finite lemmas below are
+recomputed; no pending theorem supplies an assumed lower bound.
+
+## Statement
+
+Let V be the sum-zero subspace of R^9. Take the 120 root lines represented by
+`e_a-e_b` for `0<=a<b<=8`, followed by `r_S=1_S-(1/3)1` for three-element S,
+lexicographically within each group. Puncture the frame
+
+```
+F = [0,85,94,99,105,108,112,113]
+```
+
+or any of its coordinate-permutation images. On the 112 live roots set
+`G_ij=r_i dot r_j` and fix `T_ik=r_ik`, for `k=0,...,8`.
+For every complex D satisfying `D T^t=2G` on all live pairs, the sum of the
+nine separate term costs is at least 71. Here the cost of a term is the F2
+rank of `(G_ij+1) mod 2` on its nonzero row and column supports. Transpose is
+ordinary transpose. The bound is attained with all nine terms active.
+
+The orbit of F contains exactly 1,080 frames. Each has one pair root and seven
+triple roots forming a Fano plane on the seven coordinates outside that pair.
+Together with the 945 matching frames of PR1304, these exhaust all 2,025
+orthogonal eight-frames. The sharp bound proved here concerns the new orbit.
+
+## 1. Geometry and complete orbit coverage
+
+Use labels `u_ab=1+e_a+e_b` and `u_S=1_S` in F2^9. All 14,400 entries of
+
+```
+u_i dot u_j = (G_ij+1) mod 2
+```
+
+are checked from exact integer coordinates. The live roots span V, and the
+labels on each column support `{i:r_ik != 0}` span F2^9. These are finite
+rank calculations; no root-hyperplane classification premise is needed.
+
+The frame census recursively lists every increasing eight-clique in the
+orthogonality graph. Its completeness follows by partitioning continuations
+by their least next index and intersecting with that root's later neighbors.
+The size bound only prunes a branch with too few remaining vertices. It finds
+2,025 frames.
+
+Adjacent coordinate transpositions generate S9. Applying their explicitly
+checked root-line permutations to F until closure gives 1,080 frames. Doing
+the same for `[0,15,26,33,42,89,112,119]` gives 945. The two sets are disjoint
+and their union equals the entire clique census. Every frame in the first
+orbit has one pair root; every frame in the second has four.
+
+The second implementation independently obtains the same complete frame sets
+from rational Gram entries. On seven points it enumerates all coordinate
+images of F's seven triples, obtaining 30 labeled Fano planes. Choosing any
+of the 36 coordinate pairs and any of these 30 planes constructs exactly the
+1,080 one-pair frames. Equality of the enumerated sets is checked, not inferred
+from their cardinalities.
+
+Coordinate permutations preserve the fixed simplex normals up to permutation.
+Signs needed to restore the chosen pair-root representatives preserve supports
+and binary pairings. Applying those same row signs to D and T preserves the
+all-pairs equation. Thus a bound and witness for F transport to its entire
+orbit without changing costs.
+
+## 2. Arbitrary complex coefficients reduce to deficiencies
+
+Since the live roots span V, `D T^t=2G` is equivalent to
+
+```
+D_ik = 2r_ik + t_i,  with arbitrary t_i in C.
+```
+
+Indeed `D_i-2r_i` annihilates V and hence is a multiple of the all-ones vector.
+The argument holds over C with the bilinear transpose and needs no positivity.
+
+Let K_k be the binary annihilator of the labels on the nonzero row support
+of column k, and let `delta_k=dim K_k`. Full label span on each T column makes
+its pairing map injective on the D support, so its term cost is `9-delta_k`.
+The total cost is therefore `81-sum delta_k`.
+
+If `w in K_j` and `z in K_k` both evaluate to one on `u_i`, then
+`D_ij=D_ik=0`, forcing `r_ij=r_ik`. Call this compatibility of the functionals
+at j and k. This necessary condition concerns zero patterns, so includes all
+complex shifts, even shifts giving no zero entries.
+
+## 3. Exhaustive finite cover and upper bound
+
+If all nine deficiencies are at most one, their sum is at most nine. Otherwise
+choose an anchor j and a binary plane U inside K_j. Each plane has exactly
+one encoding `0<a<b<a xor b`, so there are `511*510/6=43,435` planes.
+
+For each other coordinate k, define H_k(U) as the functionals z compatible
+with both basis vectors of U. This is the annihilator of the labels at rows
+where `r_ij!=r_ik` and some basis vector evaluates to one. Compatibility with
+the basis is equivalent to compatibility with all of U: a nonzero evaluation
+of a linear combination needs a nonzero basis evaluation. Thus
+K_k is contained in H_k(U).
+
+The finite census checks `dim H_k<=2` for every anchor and plane. Enumerate
+every subspace L_k of every H_k: zero, each line, and H_k itself when it is a
+plane. Retain only tuples whose members are mutually compatible. For a
+retained tuple let Q be the span of labels at rows where, for some k other
+than j, `r_ij!=r_ik` and some vector of L_k evaluates to one. Necessarily
+
+```
+K_j subset Q^perp,
+sum delta_k <= 9 - dim Q + sum_(k != j) dim L_k.
+```
+
+The actual tuple `L_k=K_k` occurs and is retained. Some relaxed tuples need
+not be realizable by a decoder, which can only weaken the upper bound.
+Planes with identical ordered partner spaces are grouped because the tuple
+enumeration and Q depend only on these spaces and the anchor. Every plane
+still contributes to the recorded multiplicities.
+
+The exact exhaustive results are:
+
+| Anchor | Planes | Ordered partner-space tuples | Compatible subspace choices | Largest upper bound |
+|---|---:|---:|---:|---:|
+| Each of 0,1 | 43,435 | 2,131 | 52,829 | 10 |
+| Each of 2,...,8 | 43,435 | 2,251 | 39,482 | 9 |
+| Total | 390,915 | 20,019 | 382,032 | 10 |
+
+The primary checks all nine rows individually. The second checker derives
+label coordinates from nine independent columns of the rational Gram pairing
+matrix, computes H_k by nullspace algebra, enumerates Cartesian products, and
+tests the forced coefficient values row by row. It checks representatives 0
+and 2. Explicit coordinate permutations preserving F have orbits `{0,1}` and
+`{2,...,8}`, establishing coverage of all anchors; its tables agree with the
+primary. Both implementations are credited adaptations of PR1304, not separate
+human review.
+
+For every possible deficiency tuple, `sum delta_k<=10`. Hence cost is at
+least 71. Mutual compatibility is material: at anchor 0 with
+`U=span(1,508)`, dropping it permits an upper bound of 11, whereas including
+it gives 10. The apparent cost 70 in that relaxation is not a decoder.
+
+## 4. Sharp witnesses and COPY power contribution
+
+Set `t_i=-2r_i0`. The costs are `(0,8,9,9,9,9,9,9,9)`, totaling 71.
+At just the live root `e_0-e_2`, change its shift to `t_i=-2r_i2`.
+All nine terms then become active, with costs `(1,8,8,9,9,9,9,9,9)`, also 71.
+Both identities are checked on all `112^2=12,544` live pairs. The second
+checker computes the active witness costs directly from pairing submatrices,
+without the full-column-span shortcut.
+
+There is also a COPY-only power comparison, when width, normalization and
+term multiplicity are fixed. Each of the nine ranks lies between zero and
+nine, and their sum is at least 71. For `0<p<=1`, monotonicity followed by
+concavity bounds their total p-power below by `7*9^p+8^p`: first reduce the
+sum to 71, then move mass from a smaller positive interior rank to a larger
+one until only one rank is interior. Each move does not increase the concave
+sum. The resulting ranks are seven nines, one eight and one zero. Therefore
+
+```
+sum rank_k^(1-a) >= 7*9^(1-a)+8^(1-a) > 8*8^(1-a),  0<=a<1.
+```
+
+This is strictly worse than the eight rank-eight coordinate COPY terms under
+those same accounting parameters. It does not compare complete suppliers
+with changed widths, role counts or shared-copy mechanisms.
+
+## Scope
+
+The result does not cover changed nine-normal families, unrestricted factors,
+masked identities, other live-set sizes or shared-copy billing. No physical
+word, frame/restoration/hosting proof, selected cold replay, new κ or all-size
+multiplication theorem is supplied. The selected construction's inherited
+algorithmic, analytic, precision and bit-interface obligations remain open.
+
+Credit commdata2338/PR1304, Philipp/mightyOil/PR1248, joaqcoo/PR1224 and the
+decoder/label lineage listed in README.md. Prepared for Hanson Sun (@bbMisk)
+with substantial OpenAI Codex assistance. Apache-2.0.

research/a8-one-pair-frame-floor/README.md

@@ -0,0 +1,121 @@
+# Sharp COPY cost 71 on the remaining A8 simplex P112 frame orbit
+
+The fixed nine-normal A8 simplex decoder has minimum separate COPY cost **71**
+on each of the **1,080 one-pair frame punctures**, for arbitrary complex row
+shifts. An exact witness with all nine terms active attains the bound. Thus
+this family cannot beat the standard P112 COPY cost 64.
+
+This resolves the other-frame question in
+[commdata2338's PR1304](https://github.com/CrocSwap/integer-mult-bounds/pull/1304).
+That predecessor covers 945 matching frames. A complete census here partitions
+all 2,025 orthogonal E8 eight-frames into precisely those 945 frames and the
+1,080 frames treated here. The latter consist of one pair root and a Fano
+plane on the other seven coordinates. No theorem from a pending PR is assumed
+to establish the new orbit's bound.
+
+This is a scoped proof with exhaustive finite lemmas, **not a new supplier or
+κ result**. It leaves the selected record and frozen sources unchanged.
+
+## Exact scope and evidence
+
+In the sum-zero subspace of Q^9, use roots `e_a-e_b` and
+`1_S-(1/3)1`, for three-element sets S, in lexicographic order within those
+two groups. Fix `T_ik=r_ik`; require `D T^t=2G` on all live pairs, with ordinary
+transpose. Every permitted D has `D_ik=2r_ik+t_i`, with arbitrary `t_i` in C.
+Term costs are binary label-pairing ranks on the actual nonzero supports.
+
+The representative puncture is `[0,85,94,99,105,108,112,113]`. The proof in
+[PROOF.md](PROOF.md) reduces all complex shifts to finite binary deficiency
+compatibility. The two coordinate-anchor classes give:
+
+| Anchors | Planes per anchor | Partner-space tuples per anchor | Compatible choices per anchor | Maximum deficiency sum |
+|---|---:|---:|---:|---:|
+| 0, 1 | 43,435 | 2,131 | 52,829 | 10 |
+| 2 through 8 | 43,435 | 2,251 | 39,482 | 9 |
+
+The primary replay checks all nine anchors: 390,915 planes, 20,019 distinct
+ordered partner-space tuples across anchors, and 382,032 compatible choices.
+The resulting cost is at least `81-10=71`. Witness costs are
+`(0,8,9,9,9,9,9,9,9)` and, with all terms active,
+`(1,8,8,9,9,9,9,9,9)`. Both all-pairs identities are checked exactly.
+
+The second implementation derives labels from the rational Gram matrix,
+uses nullspaces and Cartesian products instead of the primary bitmask search,
+and checks two anchors with explicit puncture-preserving permutations covering
+all nine. It also re-enumerates all frames and constructs the new orbit from
+36 pairs and 30 Fano planes, separately from the primary coordinate-orbit BFS.
+
+Both implementations are adapted from PR1304, with exact original file pins
+in [SOURCES.json](SOURCES.json) and attribution in their headers. Every finite
+premise for the changed puncture is recomputed. This is reuse of credited
+methods; no independent peer review is claimed.
+
+## Reproduce
+
+From the repository root, standard library only:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/a8-one-pair-frame-floor
+```
+
+The registered replay runs the primary checker, second checker and package
+failure tests. Individual checks also work with Python 3.12 or later:
+
+```sh
+python3 -I -B research/a8-one-pair-frame-floor/verify.py
+python3 -I -B research/a8-one-pair-frame-floor/independent.py
+python3 -I -B research/a8-one-pair-frame-floor/test_package.py
+```
+
+Expected mathematical markers:
+
+```text
+PASS_A8_ONE_PAIR_FRAME_FLOOR frames=1080 anchors=9 planes=390915 configurations=20019 compatible_leaves=382032 cost=71 controls=10
+PASS_A8_ONE_PAIR_SECOND_CHECK anchors=2 transported=9 planes=86870 compatible_leaves=92311 cost=71
+```
+
+Default replay is read-only and compares the entire deterministic certificate.
+`verify.py --write` explicitly regenerates it. Ten semantic controls cover
+identity, support costs, labels, puncture legality, compatibility, complex
+shifts and omitted/misidentified frame coverage. Package tests exercise altered,
+missing and malformed receipts and optimized relocated replay.
+
+## Limits and credit
+
+Only this fixed nine-normal, all-pairs, separately charged family is covered.
+Other normals, arbitrary two-factor or masked decoders, other live-set sizes
+and shared-copy pricing are outside the result. The COPY power comparison in
+the proof fixes the width, normalization and multiplicity; it is not a complete
+supplier invoice. Physical gathering, frame legality, restoration, hosting,
+precision/tape, all-size/compiler, common-label/mutable-source, analytic and
+bit H1–H5 obligations are not checked. No selected cold replay, Lean proof,
+hosted-CI success, human review or maintainer acceptance is claimed.
+
+Predecessor credit:
+
+- commdata2338, PR1304: matching-frame floor, both adapted implementations,
+  and the explicit other-frame question.
+- Philipp / mightyOil, PR1248: the deficiency-space method on P120.
+- joaqcoo, PR1224: the one-sided nine-term normal form and A8 family.
+- DreamingOfClouds, PR717/595/446: decoder and separate-copy label model;
+  Joel Pulikkan / GamingPuzzled, PR620: the coordinate COPY64 construction;
+  themilkman216, PR968, and woklerx, PR1077: surrounding all-pairs bounds.
+
+Base main: `ebedc0895eb4c06725af020bc1af165722b0a3ce`. The task, selector nonce,
+exact predecessor heads and overlap boundaries are in [TASK.json](TASK.json).
+The claim is in [discussion 1241](https://github.com/CrocSwap/integer-mult-bounds/discussions/1241#discussioncomment-18914233).
+
+Prepared for Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance in
+the mathematics, both adaptations, verification and writing. Apache-2.0.
+
+## Open next questions
+
+- **A different specified nine-normal family.** Can an A7+A1 or A2+E6 family
+  from PR1224 achieve COPY cost below 64 on a named P112 puncture? First derive
+  its exact kernel-shift classes and column-label ranks, then a favorable
+  finite compatibility bound. The fixed simplex normals are essential here;
+  neither the deficiency table nor the frame symmetry automatically transfers.
+- **Shared-copy accounting.** Can a concrete physical implementation share
+  copied information across these nine terms at a net saving? First write its
+  entry/exit contract and full recursive bill. This theorem assumes separate
+  term charges; a support overlap alone is not a paid implementation.

research/a8-one-pair-frame-floor/SOURCES.json

@@ -0,0 +1,50 @@
+{
+  "schema_version": 1,
+  "base_commit": "ebedc0895eb4c06725af020bc1af165722b0a3ce",
+  "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-frame-pair-decoders/verify.py",
+      "usage": "provenance",
+      "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb",
+      "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395"
+    }
+  ],
+  "external_predecessors": [
+    {
+      "pr": 1304,
+      "author": "commdata2338, with substantial OpenAI Codex assistance",
+      "head": "a052f0da36a3845c2ec785fd44e5b9e50de3b688",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1304",
+      "usage": "Method and adapted implementations; no pending theorem is assumed. Exact original file pins below.",
+      "files": [
+        {
+          "path": "research/a8-p112-decoder-screen/verify.py",
+          "git_blob": "188d3a8fda62067dd6f7c37e79a65a3e0cbe2fa7",
+          "sha256": "c8dff5ebf75511bf7c5e962a42189977ef5b20ce02e6f9734e4648e695ca3148"
+        },
+        {
+          "path": "research/a8-p112-decoder-screen/independent.py",
+          "git_blob": "02035af27f93aee0f0205b69a3be99fe4362fd13",
+          "sha256": "e646772a4b25a26808bdded1362481a63c92fbaa3d61ad33aa6bfea38a40ff03"
+        },
+        {
+          "path": "research/a8-p112-decoder-screen/PROOF.md",
+          "git_blob": "4f18ea6417759e73f9e03b5878f75c3fe3b0efd7",
+          "sha256": "2e7640f6bf1a683fe7e830414065c41e8fa38155023a97a27aadaa9a5f8a068b"
+        }
+      ]
+    }
+  ]
+}