[JosieElliston]

Scope and task card

Research base: main a18b4b0136d647529971e9fcb99fa83f5b9a0b81; the branch is rebased onto main 0b1cccf8 with all pinned inputs unchanged. The selected #1094 record is unchanged. Chooser nonce 1f0be36e3f2ed2c4ea3d763eb52aedc1 drew the revision-3 formal-interface-lemma card. It is refined to a theorem-to-certificate audit of PR1212 (Brett Halligan / @burntout76 and Ninefold, head 57099cb5, now on main as research/complex-rank8-decoder-rigidity/): §10's stabilizer transport and §8's bridge from gauge rigidity to PR968's eight-term floor. PR1670 (session 16 of this run) audited PR1560 and explicitly left these two sections uncovered.

Precise delta

Adds only research/e8-rank8-transport-audit/. No predecessor, selected or upstream/ changes.

• §10 transport, recomputed independently. The 120 E8 lines are built from scratch, without PR1212's group code. The verifier checks 2,025 frames (one Weyl orbit), 204 one/two-reflection maps fixing FRAME0, signed Gram transport for every generator (binary pairing preserved), one orbit on the 112 P112 lines, and orbits 28/336/896 on the 1,260 second frames, typed (4,4)/(2,2,2,2)/(1⁸). It also places PR717's P104 in the 896 orbit and rechecks PR1212's published (2,2,2,2) unit and pivot.

• Alternate pivot for type (4,4). The unit is PR1212's own representative: delete FRAME0 and {2,3,16,17,46,47,52,53} (PR1212 numbering). Of its 801 live pivots, 25 leave no class incomplete. PR1212's pivot {4,5,14,15,48,49,50,51} covers 12 of 14 blocks, and 24 others cover all 14. That contradicts PR1212 §10's remark that other pivots "leave eight classes incomplete". At {12,13,22,23,30,31,36,37}, which is also PR1212's (2,2,2,2) pivot, the checks give:

  • 288 Lemma 5 group witnesses;
  • 56 Steiner triples and 24 Hadamard classes;
  • 1,952 ordered Lemma 6 sign-rule checks;
  • an independently encoded two-term + diagonal zero-pattern CNF (1,152 variables, 16,865 clauses with some zero), refuted by a 2,501-addition DRUP proof from Lingeling that a stdlib RUP checker replays.

  PR1212's original Lemmas 5–7 then give rank-eight gauge rigidity for this unit, and the transport extends it to all 28.

• What is new. This is a second proof of a theorem PR1389 already established. PR1389 kept PR1212's 12-block pivot, added gluing Lemma 6′, and relied on PR1212's four-family zero exclusion. The alternate route needs only the original Lemmas 5–7 and the two-family certificate.

• §8 written audit. Eight costly terms of a gauge-rigid rank-eight E-graph matrix have the same supports as an exact all-pairs decoder (RA,RB), so PR968's real floor applies. At p=16 that floor is PR968(a)'s ≥56; (b)'s 72−p is stated only for p≤15. A complex COPY floor needs the separate complex extension.

Review by Claude (session 19): what changed

Codex ran out of usage mid-edit. Its notes, README, PROOF and RESULT.json described an earlier run that had deleted the wrong frame: the 28-orbit's minimum, which is PR1212's pivot frame, labelled as PR1212's deleted frame. Codex fixed the binding in verify.py and regenerated the CNF and proof, but did not update anything else. The shipped verifier then failed its receipt comparison. In review I:

• regenerated RESULT.json;
• corrected PROOF/README/TASK (deleted frame, digests, 2,501 lemmas instead of 2,910, proof size);
• made the verifier require the displayed pivot to equal PR1212's {12,…,37} and record both numberings;
• strengthened the gluing check from a count to PR1212's exact sign rule, in both orders;
• made the PASS marker report computed counts;
• pinned PR1212's PROOF.md at its main path (byte-identical blob 5940f280) instead of a vendored copy.

Independent cross-check, not part of the package. PR1212's own code (extension_units, blocks_relative, build_zero_cnf) run on the same unit confirms:

• the (24,0,12) and 24×(24,0,14) pivot census;
• D1/D2 witnesses at the new pivot;
• with CaDiCaL, the reduced two+diag CNF is UNSAT with some zero and SAT without it at the new pivot, and SAT at PR1212's pivot, matching its Lemma 8.

Reproduce

python3.12 -I -B research/e8-rank8-transport-audit/verify.py
python3.12 scripts/research_package.py --package research/e8-rank8-transport-audit

Stdlib only, about 5 s; passes on 3.10, 3.12 and optimized 3.14. Controls reject a Gram-sign change, a corrupted transport permutation, the proof without some zero, an injected non-RUP unit and a truncated proof.

Limits, overlap and credit

Not covered: a new COPY floor, κ change, complex COPY floor, nine or more costly terms, or a proof-assistant formalization. PR1212's written Lemmas 5–7 and PR968's cited flat classification (F6) are relied on, not reproved. PR1497 separately audits Lemmas 5–6. A live overlap refresh (451 open PRs, 417 discussions, 2026-10-14 05:55 EDT) found PR1389 (priority for the theorem), PR1670 (complementary) and @1337isnot1337's all-pivot census of an admissible P104 unit in discussion 1163, which is a methodological precedent on a different orbit.

Open next questions: (1) Can this pivot shorten a formalization of type-(4,4) rigidity? (2) Does the two-family refutation at this pivot have a short readable core? At PR1212's pivot the same two families do not exclude zeros.

Credit: Brett Halligan / @burntout76 and Ninefold (PR1212); PR1389 (Josie Elliston, Claude-assisted); PR1497's auditors; @themilkman216 (PR968); DreamingOfClouds (PR717); @an664 (PR1560) for the surrounding rigidity line.

Prepared for Josie Elliston (@JosieElliston) by OpenAI Codex (offline session 17b of an overnight donated run: audit, verifier, proof generation, controls, writing). Claude (Anthropic, session 19) reviewed, corrected and published it. Substantial AI assistance; no independent human review. Apache-2.0.

🤖 Generated with Claude Code

[Mister-Meeseeks]

Batch review at c7d75c1dd348ed4312b095ca467ce966493cf9e8.

Merged to main, preserving the original contributor commits and package attribution.

Reviewed scope: Alternate complete P104 type(4,4) pivot supplies all four finite rigidity premises, with independently generated geometry, stabilizer transport and2501-step exact RUP replay. Written predecessor Lemmas5–7 remain dependencies. Corrects a pivot remark and corroborates the already established theorem; no new complex COPY claim.

The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions.

Batch review, attribution and evidence. Thank you for the contribution.