Skip to content

Prove the sharp penalty for one-extra Dn decoders - #2659

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
ywz65:ywz65/n30-r010-fresh-obligation
Oct 16, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
ywz65:ywz65/n30-r010-fresh-obligation

Conversation

@ywz65

@ywz65 ywz65 commented Oct 15, 2026

Copy link
Copy Markdown
Contributor

This proves a sharp positive penalty for every genuine (n+1)-term member of PR2518's full D_n, standard-coordinate, one-extra rank-one decoder family. For every real direction and parameter, n>=3, its exact minimum is n(n-1)+(n-2 for odd n, n-1 for even n). The attaining direction is e1+e2 with parameter 1. The only baseline ties are zero extra terms or exact singleton replacements. This retires further direction tuning inside this precise family.

The strict gap and equality classification are new. Aaron Wang/navinor's PR2518 (5ccad6a) supplies the finite screen, source convention and credited D4/D5 minimum fixtures; its one-extra identity credits PR2240/2247. DreamingOfClouds' PR2277 already establishes broader non-strict D5 and D4/D6 floors; those are not claimed as new. The proof uses exact star-rectangle ranks and principal-support submatrices over F2, without any finite-direction premise. Dense pairing, full unpunctured lines and the original standard p_i frame remain essential.

Validation on CPython 3.12.14: the registered replay passed 5976 ternary star rectangles, 1076 principal supports, 360 exact rational family fixtures for n=3–12, source support-cell binding and predecessor minimum replays, six semantic controls, a separate Boolean checker of 180 full Gram/bill fixtures and 34 parity blocks, and optimized Git-free read-only/source/receipt/output controls. Root proof review is recorded in the delivery metadata. No hosted CI or formal-kernel pass is claimed.

python3.12 -I -B scripts/research_package.py --package research/dn-one-extra-gap

Fresh canonical main is b4560d9, priority revision 5. The picker and ceiling/lever controls were followed. The family decision is to pause this exact search family; no native expansion is proposed. Physical copies, frames, consumer/restoration, hosting, precision and supplier admission remain outside this local theorem. Selected/frozen files are unchanged. Final overlap combines the 817-PR snapshot, bounded 1239-Discussion snapshot, latest 100 current PRs and targeted PR2518 head/comments; it is not an exhaustive novelty guarantee. A prior local ring-extension attempt was withheld when PR2630/2631 superseded it, and is not counted.

Prepared by ywz65 with substantial OpenAI Codex assistance in proof, implementation, verification and prose; Apache-2.0. No independent human review is claimed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants