Exact overcomplete E8 decoders: outside-code rank budget and ten-term normal form

[bbMisk]

DONE — PR1633, head 652264fa1f70820139b2730363a0056b7fadc689. Claim completed.

The package proves the sharp feasible region s+t <= m-8 for the two outside-root-code ranks of any exact all-pairs E8 decoder, including attainment with all terms active. It gives the necessary-and-sufficient rank-one residual form for two-sided ten-term decoders. Real symmetric exact decoders always remain in the root code; complex symmetric ones can attain residual rank min(n-8, floor((m-8)/2)) under ordinary transpose. The proof uses elementary rank algebra and isotropic cancellation; PR1224 retains credit for the original projection equations, nine-term dichotomy and ten-term two-sided existence.

Local registered Python3.12 replay passed: 168 general and 32 symmetric complex examples, 2,694,400 identity entries, two exact rank algorithms, four extracted ten-term forms, ten controls and six regression groups. A standalone integer checker also checks a complex symmetric P112 witness and its complete cost increase from 82 to 90 under an identity-preserving orthogonal gauge. The two implementations are by the same assisted author; no independent human review is claimed.

Reproduce: python3.12 -B scripts/research_package.py --package research/decoder-excess-rank. Only this new package is added, starting from main ee055dc4 and fast-forwarded onto 0a201997 with guidance and inputs unchanged. The final paginated overlap snapshot covered 741 open PRs and 267 discussion records; exact predecessor heads and limits are recorded in the package.

Remaining scope: the unrestricted ten-term support/copy-cost search and physical realization. The original rank-shape construction gate is not met; no new kappa, supplier admission, selected cold replay or Lean theorem is claimed. Hosted CI was queued at publication. Credit joaqcoo, woklerx, themilkman216, mightyOil, Sagar Thakrar, DreamingOfClouds, Douglas Colkitt and Arham Tahir, with details in the package. Prepared by Hanson Sun with substantial OpenAI Codex assistance.

Original claim (completed)

CLAIM — exact overcomplete decoder excess-rank budget

Question: for an all-pairs exact m-term E8 decoder D T^T = 2 R R^T, how much rank can lie outside the live root code on the two factors, and what does this force at ten terms? Include the distinction between real symmetric and complex symmetric factors under ordinary transpose.

Base: ee055dc. Predecessor: joaqcoo / PR1224, head 00e6ed0, Theorem A and the nine-term one-sided result. The intended delta is an all-m sharp residual-rank budget and the complete two-sided ten-term residual form, with exact attaining examples. This is elementary rank algebra specialized to the decoder search interface, not a claim of a new general linear-algebra theorem.

Method/domain: a written proof over R and C; exact Gaussian-rational P112/P120 examples for m=8..14; literal all-pairs identities, projected residual ranks, and controls for omitted charges, transpose and invalid residual coupling. Existing fixed-coordinate two-total PR1197 and fixed parity-lift PR1327 do not cover this unrestricted algebraic classification. No copy-cost floor, physical supplier or new kappa is planned.

Scope change: revision-3 card complex-rank-shape-decoder selected in the complex-mechanisms track; refined away from physical synthesis to this necessary-condition side result. PR1605 already covers the reblocking planning budget. Expected artifact: one self-contained proof/checker package with exact sources, replay and next question.

Claim expires: 2026-10-14T06:15:00Z. Prepared by Hanson Sun (@bbMisk) with substantial OpenAI Codex assistance; no subagents.

[1337isnot1337]

CLAIM — Cycle 12, complex-mechanisms / complex-rank-shape-decoder (accepted selector card cad3ba853d7f324f16fa; refined to a bounded overcomplete-decoder construction).

Seed 06ace58bfc2b63b47b02129f729e35d4; priority revision 3; exact base 0b1cccf86e2f5132ed286a26ef0a681a495740ea; selected-record SHA-256 10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32.

Object. The exact symmetric P112 ten-term witness pinned in open PR #1633 (head 652264fa1f70820139b2730363a0056b7fadc689), with D D^T = 2 R R^T and support-rank invoice (8,8,8,8,8,8,8,8,9,9). Test whether one rational term-coordinate Householder gauge O_s=I-2ss^T/(s^Ts), for each nonzero s in {-1,0,1}^10 modulo sign, can lower its per-term support ranks enough to change the selected centre profile. This changes the decoder assumption to ten active terms and directly tests the predecessor's warning that term gauges need not preserve copy cost.

Bounded method. Enumerate the 29,524 reflections exactly. Verify ordinary-transpose identity on all 112x112 P112 pairs, all terms active, and each binary support-rank invoice; apply the ten resulting child ranks to the selected per-call profile and screen with the pinned ceiling() model. The best-case ten rank-one terms with zero extra charges yield a_cap=532095622847/125000000000000, above the 5% gate 0.00177455681454345; all coefficient/frame, precision, hosting and restoration costs must still be charged against the candidate. Stop if the exact family has no 5%-clearing candidate once its support bill is applied.

Predecessors/overlap. PR #1633 proves the rank-one residual normal form but leaves this support-cost question open; its H=I example costs 82 and its gauge example costs 90. PR #1224 and PR #1077 supply earlier decoder equations and E8 data. The open rank-16 diagonal batches in #1779/#1817 and the later child-contract obstruction concern a different block-diagonal mechanism; I am not repeating that route. The fresh complete overlap refresh covered 543 open PRs and 529 Discussion records.

Deliverable. An exact finite construction or a bounded negative result for this Householder family, with pins, full support invoice, exact moment screen, controls and remaining physical obligations. Expiry: 2026-10-14 15:30 UTC. Substantial OpenAI Codex assistance will be disclosed.

FINDING — DONE

PR #1923 adds the exact bounded result at commit 0d33d602. All 29,524 rational ternary Householder gauges preserve the pinned ordinary-transpose P112 identity; all ten terms stay active, and the nine exact support-rank histograms use only ranks 8 and 9. The minimum invoice remains (8,8,8,8,8,8,8,8,9,9), total 82, so none improves on the witness invoice.

Applying that best invoice to the selected centre profile raises its mass from 64 to 82. Even waiving every other charge, the exact fixed-word ceiling is [0.000834274164361244, 0.000834274164361245], below the selected ceiling 0.001690054109089 and 5% target 0.00177455681454345. This is a scoped negative for the exact symmetric witness and searched rational Householder orbit only; it is not a lower bound for asymmetric or other-support decoders, and claims no supplier change or new kappa.

The result is distinct from newly open PR #1909, which proves a tetrad-local COPY112 floor for a broader masked-decoder class; this census addresses gauge variation and the exact support invoice of the PR #1633 witness. Final overlap refresh: 571 open PRs, 541 Discussions, complete pagination, no warnings. Direct verifier, five controls, package/pin check and staged whitespace check pass locally on Python 3.14.7; Python 3.12, required by the registered replay, is unavailable locally.

PR: #1923