Certify a mixed-rank P112 counterexample at common cut40

research/p112-mixed-sharp39/PROOF.md

@@ -0,0 +1,85 @@
+# A mixed 5,5,6 counterexample at common cut 40
+
+Let P be the 112 nonframe E8 root lines in the pinned `geometry.py`, with its
+leading-one nine-bit labels. For a characteristic-zero field K let
+`C = {(r_t dot h)_t : h in K^8}`. Binary support rank means the F2 rank of
+the labels at nonzero coordinates. Let pi delete one coordinate set S.
+
+**Proposition.** There is a set S of 40 coordinates and three rational residual
+vectors q1,q2,q3 of binary support ranks 5,5,6 for which
+
+```
+dim_K(pi(C) intersect span_K(q1,q2,q3)) >= 2.
+```
+
+All data are integers, so the same example works over every characteristic-zero
+field. The sufficient allowance 39 proved in pinned PR3278 is therefore sharp,
+conditional on that predecessor's theorem. Its proof and receipt are retained
+verbatim; the present replay does not re-prove its sufficient direction.
+
+## Literal construction
+
+Use these orthogonal doubled-root directions:
+
+```
+a = (0,0,0,0,0,2,-2,0)
+b = (0,0,0,2,-2,0,0,0)
+```
+
+Their codeword union U has 84 live coordinates. Its projective fibers have
+sizes 31,31,11,11. Each large fiber has lost two frame roots, unlike the
+four-root punctures of PR3278's minimum-union planes.
+
+In the fixed sorted P112 order, take the following disjoint supports:
+
+```
+A = [37,38,49,50,53,54,65,66,69,70,81,82]
+B = [17,18,21,22,27,28,31,32,103,104,107,108]
+D = [5,6,11,12,25,26,33,34,43,47,56,60,75,79,88,92,101,102,109,110]
+```
+
+A and B lie in a's axis fiber, where c_b is zero. D lies in b's axis fiber,
+where c_a is zero. Their exact binary label ranks are 5,5,6. Define
+
+```
+S = U minus (A union B union D)
+q1(t) = c_a(t) on A, zero elsewhere
+q2(t) = c_a(t) on B, zero elsewhere
+q3(t) = c_b(t) on D, zero elsewhere.
+```
+
+Since the support union has size 44, S has size 84-44=40. At each of the
+72 retained coordinates the actual integer data satisfy
+
+```
+q1 + q2 = pi(c_a),    q3 = pi(c_b).
+```
+
+The codewords have disjoint nonempty retained supports. Their evaluation minor
+at coordinates 5 and 17 is nonzero, of absolute value 16. Thus they remain
+independent over K and belong to the piece span, proving the proposition.
+`WITNESS.json` records all 112 entries of each piece and every cut index.
+The replay checks these equations and ranks directly; feasible cardinality
+counts or abstract set covers alone would not prove the statement.
+
+## Evidence and limits
+
+The primary checker uses the source-authenticated geometry, exact integer
+equations and nine-pivot binary elimination. The separate checker reconstructs
+roots by coordinate type, recovers simple-root coefficients through an integral
+recurrence, and checks span sizes 32,32,64. All matrices and sets are finite.
+No optimization, float tolerance, full flat census or scientific Git dependency
+is needed to check the counterexample.
+
+PR3278 supplies the sufficient theorem at 39 and explicitly records inherited
+capacity and Weyl/chamber dependencies. Hash authentication does not establish
+those mathematical dependencies. The new obstruction at 40 stands separately.
+PR3283's related uniform-rank-five witness at 48 uses different data and ranks;
+its conclusion is not needed here. Concurrent A2 rank-six joint32 and D6
+four-puncture capacity18 proofs are unused.
+
+This is a shortening counterexample. It does not supply an actual caller,
+a full C5 factorization, a complete decoder, a physical/native implementation,
+restoration or consumer costs, a supplier or a new multiplication exponent.
+No human or proof-kernel approval is claimed. Credit the pinned PR3278
+predecessors, PR3283, DreamingOfClouds/PR3154 and the retained E8/P112 lineage.

research/p112-mixed-sharp39/README.md

@@ -0,0 +1,90 @@
+# An actual mixed-rank P112 counterexample at cut 40
+
+Three rational pieces of binary support ranks 5, 5 and 6 span two independent
+restricted P112 root-code words after ONE common cut of size 40.
+[WITNESS.json](WITNESS.json) contains every coefficient and cut coordinate.
+The supports have sizes 12, 12 and 20 and are disjoint, with union 44.
+Their code plane has live union 84. [PROOF.md](PROOF.md) explains the identity.
+
+This proves that PR3278's sufficient allowance 39 cannot increase to 40.
+The combined sharp threshold 39 inherits that pending predecessor's sufficient
+theorem and its stated dependencies. The new counterexample requires only
+the pinned geometry and exact arithmetic. It works over every characteristic-zero
+field. It supplies no literal caller, full C5, decoder floor, native program,
+physical invoice, supplier admission or new kappa.
+
+## Reproduction
+
+From the repository root, with Python 3.12 and the standard library:
+
+```sh
+python3.12 -W error -B scripts/research_package.py \
+  --package research/p112-mixed-sharp39
+```
+
+The three registered commands also work directly in a Git-free export:
+
+```sh
+python3 -W error -B research/p112-mixed-sharp39/verify.py
+python3 -W error -B research/p112-mixed-sharp39/independent.py
+python3 -W error -O -B research/p112-mixed-sharp39/test_verify.py
+```
+
+The primary check verifies all 144 retained coefficient equations, the actual
+support ranks, the common cut and a nonzero minor. The independent implementation
+rebuilds root coordinates and labels with an integral recurrence and uses span
+cardinalities instead of binary elimination. Six control groups cover wrong
+coefficients, missing or repeated cuts, dependent directions, rank mislabelling,
+source corruption, extra inventory and input-to-provenance relabelling.
+`SOURCES.json` has a fixed path, usage and schema inventory. Both source SHA256
+and Git blob checks remain active with Python optimization.
+
+PR3278 `67280b1da48a14435d7fde3ec81314c768a8dd3e` is retained verbatim as
+`vendor/pr3278-PROOF.md` and `vendor/pr3278-RESULT.json`, with source paths and
+exact hashes. No pending-PR Git object is needed in fresh CI or the direct
+export. Authentication preserves its evidence; it does not independently prove
+its sufficient theorem. Its historical capacity checks and Weyl argument are
+not rerun. Selected cold replay, Lean, Docker, human and proof-kernel review
+are unrun. Internal computational review is narrower than those obligations.
+
+## Scope and implementation decisions
+
+The revision-6 card's first local-word ceiling control passed. This package takes
+the explicit PR3278 cut-40 realization handoff as a side result. It does not meet
+or claim the card's 5% supplier target. The family decision is to finish this
+missing implication and stop. Source access, physical frames, native restoration,
+hosting and complete consumer costs remain unknown.
+
+The old union-82 equality probe did not decide this boundary. At cut 40 the
+permitted support sum allows union 84. Its large fibers have TWO frame punctures
+each, leaving 31 sites, rather than the four-puncture 29-site fibers used in
+PR3278's union-82 argument. The four-puncture capacity 18 does not apply here.
+Concurrent analytic D6 capacity18 and A2 joint32 investigations are distinct
+and unused. The uniform rank-five cut48 witness in PR3283 has a distinct rank
+contract and retains credit for the related axis-splitting idea.
+
+Separate Before Serializing Shared State gave the work its own package, branch,
+cache and status, with brief shared Git and claim operations under OS locks.
+Prove It Works required actual coefficient replay and the committed Git-free
+export. Power of Ten deviations are limited to standard-library Python's
+managed allocation and one source-authenticated geometry import. Files are
+limited to 100,000 bytes, roots to 120, points to 112, binary spans to 512 and
+minor checks to 2,556. Functions stay below 60 lines. Validation uses explicit
+exceptions under optimization. Frozen geometry is unchanged; no compliance
+claim is made about unrelated predecessor code.
+
+## Open next questions
+
+Which currently uncovered literal caller satisfies the sufficient cut-39
+contract? Reconcile its source inventory and give one common cut with the
+retained code dimension before applying the theorem. The counterexample is not
+a fit of the full decoder or a global upper bound. No further task is reserved.
+Structured scope and the stop rule are in [TASK.json](TASK.json).
+
+Canonical investigation: [Discussion3156](https://github.com/CrocSwap/integer-mult-bounds/discussions/3156#discussioncomment-19003989).
+
+Credit Nick Petalas/PR3278/3267/3260/3262/3269, PR3283's related uniform-rank
+witness, DreamingOfClouds/PR3154 and the retained E8/P112 geometry lineage
+including joaqcoo. The simple-root convention follows the pinned root-simplex
+geometry and PR3161/3162. Frozen inputs and the selected result remain unchanged.
+Apache-2.0.

research/p112-mixed-sharp39/RESULT.json

@@ -0,0 +1,20 @@
+{
+  "binary_ranks": [
+    5,
+    5,
+    6
+  ],
+  "code_union": 84,
+  "cut": 40,
+  "intersection_at_least": 2,
+  "maximum_absolute_minor": 16,
+  "retained_equations": 144,
+  "status": "PASS_P112_MIXED_CUT40_COUNTEREXAMPLE",
+  "sufficient39": "inherited PR3278; proof and receipt authenticated, not rerun",
+  "support_sizes": [
+    12,
+    12,
+    20
+  ],
+  "support_union": 44
+}

research/p112-mixed-sharp39/REVIEW.json

@@ -0,0 +1,112 @@
+{
+  "reviewer": "worker1 mcp:4c94af4d-cb02-44cb-a492-42bd73f88167",
+  "author": "worker4 mcp:dc1b434e-d811-4aae-9e49-e0d9febed79f",
+  "reviewed_at": "2026-10-17T20:45:24.772213+00:00",
+  "baseline": "463113d675af7410ac91d53a4fed51ec6494eb9a",
+  "scientific_commit": "a7e06dac72e0f14c85c623d8d34ce5bb0b667411",
+  "review_commit": "f3cb460d290504af8a9703136d9b95a4ce26564a",
+  "verdict": "No blocking finding at the stated exact counterexample and conditional sharpness scope.",
+  "claim": "Actual integer commoncut40, support12/12/20, binaryranks5/5/6, codeunion84, two independent restricted codewords; sufficient39 inherited only.",
+  "files": {
+    "research/p112-mixed-sharp39/PROOF.md": "893ec7be273cb29c18027b438d6bdae73ea82a6cebcc879ff1e3397efefb77cc",
+    "research/p112-mixed-sharp39/README.md": "483f71d8109ed8791df4b23a8450ee17135d7e0bc57663244a9d9bc55c3a94af",
+    "research/p112-mixed-sharp39/RESULT.json": "fbcc1add3e855736796fece39da167c06833489134f60e2eaa39e5cec13b6c18",
+    "research/p112-mixed-sharp39/SOURCES.json": "fc2a5ffd922e15cebef9f4e9dc452e5f528b915b4251db5591ad89214d894e11",
+    "research/p112-mixed-sharp39/TASK.json": "84210d69392369129559b995e829997b284d981c61cb0b3936ad0f0f056baa74",
+    "research/p112-mixed-sharp39/VERIFY.json": "327265f05b195e3b7aa90b6ffb4dc40d64d04823f3b16bad6f564743a777236c",
+    "research/p112-mixed-sharp39/WITNESS.json": "9935235a4eefbb5dff7281b98abc55562de67b48bfe5820a55e103e08a4bad9b",
+    "research/p112-mixed-sharp39/independent.py": "81f4ed4491ce228178eda10996ffc4c82e53704f9d489834823c46dc42f97029",
+    "research/p112-mixed-sharp39/sources.py": "368ec5e58d26615bee94eed21d17a5a5d496008f8c0f408e75f4053e1d06c993",
+    "research/p112-mixed-sharp39/test_verify.py": "648ab40d0169c6b269e68547a43c54090584e22f26b7c1a80904022162f7094b",
+    "research/p112-mixed-sharp39/vendor/pr3278-PROOF.md": "e3f722da7cca7d89dbc38796be5c175f78f78dd5d52036cdd0fbc33cf3c39086",
+    "research/p112-mixed-sharp39/vendor/pr3278-RESULT.json": "1de22bf31b50f7e11bb52126f0c03dd11219a2d472c86f3eaa8d2d733d9c8dc8",
+    "research/p112-mixed-sharp39/verify.py": "dd1bd9cd0fac30df43861d7e80a28b8103572454ed78d781d599ab1b2bdfe24f",
+    "research/p112-root-simplex-exclusion/geometry.py": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021"
+  },
+  "diff_sha256": "8e6d9c729b1d27349e35c5f2ee335257e62a2ca47b0f7e9f41c1982a15430354",
+  "export_sha256": "f4c20490752a21572c42576c4eb1a365212d5045bf840c1d5f908f29ffd12e0e",
+  "binding": "All14workingfiles equal reviewed Git commit and read-only Git-free export; exact official archive integrity passes;2retained predecessor payloads equal original source Git objects.",
+  "inspected": [
+    "PROOF.md;README.md;WITNESS.json;RESULT.json;TASK.json;VERIFY.json;SOURCES.json",
+    "verify.py;independent.py;sources.py;test_verify.py",
+    "Pinned geometry.py;retained PR3278 proof and receipt"
+  ],
+  "replays": [
+    {
+      "command": [
+        "/Users/nick/.local/share/uv/python/cpython-3.12-macos-aarch64-none/bin/python3.12",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "/Users/nick/.cache/integer-mult-bounds-runs/worker-4-batch5-20261017T2035Z-dc1b434e/readonly-frozen/research/p112-mixed-sharp39/verify.py"
+      ],
+      "returncode": 0,
+      "stdout": "{\"binary_ranks\": [5, 5, 6], \"code_union\": 84, \"cut\": 40, \"intersection_at_least\": 2, \"maximum_absolute_minor\": 16, \"retained_equations\": 144, \"status\": \"PASS_P112_MIXED_CUT40_COUNTEREXAMPLE\", \"sufficient39\": \"inherited PR3278; proof and receipt authenticated, not rerun\", \"support_sizes\": [12, 12, 20], \"support_union\": 44}\n",
+      "stderr": ""
+    },
+    {
+      "command": [
+        "/Users/nick/.local/share/uv/python/cpython-3.12-macos-aarch64-none/bin/python3.12",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "/Users/nick/.cache/integer-mult-bounds-runs/worker-4-batch5-20261017T2035Z-dc1b434e/readonly-frozen/research/p112-mixed-sharp39/independent.py"
+      ],
+      "returncode": 0,
+      "stdout": "PASS_INDEPENDENT_MIXED_CUT40 {'span_sizes': [32, 32, 64], 'cut': 40, 'union': 44, 'maximum_absolute_minor': 16}\n",
+      "stderr": ""
+    },
+    {
+      "command": [
+        "/Users/nick/.local/share/uv/python/cpython-3.12-macos-aarch64-none/bin/python3.12",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "/Users/nick/.cache/integer-mult-bounds-runs/worker-4-batch5-20261017T2035Z-dc1b434e/readonly-frozen/research/p112-mixed-sharp39/test_verify.py"
+      ],
+      "returncode": 0,
+      "stdout": "",
+      "stderr": "......\n----------------------------------------------------------------------\nRan 6 tests in 0.108s\n\nOK\n"
+    }
+  ],
+  "extra_checks": {
+    "live_fibers": {
+      "(1, 0)": 31,
+      "(1, -1)": 11,
+      "(0, 1)": 31,
+      "(1, 1)": 11
+    },
+    "full_fibers": {
+      "(1, 0)": 33,
+      "(1, 1)": 12,
+      "(1, -1)": 12,
+      "(0, 1)": 33
+    },
+    "axis_frame_punctures": [
+      2,
+      2
+    ],
+    "minor_sites": [
+      5,
+      17
+    ],
+    "minor": -16,
+    "piece_sizes": [
+      12,
+      12,
+      20
+    ],
+    "pairwise_disjoint": true
+  },
+  "mathematical_assessment": "The two coefficient equations place two independent restricted codewords in the3piece span. Disjoint nonempty supports give literal residual ranks checked both by elimination and span cardinalities. All integer equalities and nonzero minor16 survive every characteristic-zero extension. The union84 two-puncture plane is distinct from four-puncture capacity18; no sibling lemma is used.",
+  "unrun": [
+    "PR3278 sufficient39 proof dependencies, historical A2/D6/global capacity censuses and Weyl chamber theorem",
+    "Registered full runner in peer worktree, because direct frozen commands and manifests were inspected and replayed read-only instead",
+    "Selected cold replay, Lean, Docker, native/caller/physical supplier execution",
+    "Independent human or proof-kernel approval"
+  ],
+  "mutation_policy": "Read-only peer source/export; private control copies use reviewer session TMPDIR; no peer artifacts regenerated or edited."
+}

research/p112-mixed-sharp39/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/p112-root-simplex-exclusion/geometry.py",
+      "usage": "input",
+      "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f",
+      "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021"
+    }
+  ],
+  "retained_files": [
+    {
+      "local_path": "vendor/pr3278-PROOF.md",
+      "source_path": "research/p112-mixed-support39/PROOF.md",
+      "commit": "67280b1da48a14435d7fde3ec81314c768a8dd3e",
+      "pr": 3278,
+      "git_blob": "bedfda2d1d6babed32eb0abd349723b80a48dfb6",
+      "sha256": "e3f722da7cca7d89dbc38796be5c175f78f78dd5d52036cdd0fbc33cf3c39086"
+    },
+    {
+      "local_path": "vendor/pr3278-RESULT.json",
+      "source_path": "research/p112-mixed-support39/RESULT.json",
+      "commit": "67280b1da48a14435d7fde3ec81314c768a8dd3e",
+      "pr": 3278,
+      "git_blob": "1317727e7f583c27409b31e911137a707a30ea14",
+      "sha256": "1de22bf31b50f7e11bb52126f0c03dd11219a2d472c86f3eaa8d2d733d9c8dc8"
+    }
+  ]
+}