Skip to content

Prove A5 shortening and exclude P112 2,5^2,6^6,7 - #3203

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
petalas:research/frontier-result-20261017s
Oct 17, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
petalas:research/frontier-result-20261017s

Conversation

@petalas

@petalas petalas commented Oct 17, 2026

Copy link
Copy Markdown
Contributor

Summary

Prove a characteristic-zero P112 shortening lemma with common small support at most 29, then exclude the actual TWOSIDE (6,4) profile 2,5^2,6^6,7.

10 independent pieces, code dimension >=6
    delete the unrestricted last piece
9 independent pieces, code dimension >=5
    common small support <=26, six endpoint supports <=20
A5 endpoint requirement >=128 > allowance 120

The A5 spectrum is inherited from Nick Petalas/PR3188 and the deletion method from PR3195. PR3197's support 24 application is credited. DreamingOfClouds/PR3154 supplies TWOSIDE and the original filter; retained geometry preserves the E8/P112 lineage, including joaqcoo. Exact heads, blobs, hashes, proof, evidence, reproduction and open questions are in the package. Canonical investigation.

Evidence

  • Before: the coordinate inequality gives only 795<=800 at support 26 and cannot exclude this caller.
  • After: the full A5 spectrum requires 128>120; the general support 29 lemma still gives 122>120. At support 30 both the strict count and root-only premise cease to certify a contradiction.
  • Registered CPython 3.12.15 replay and all 18 optimized behavioral controls pass, including complete historical-table validation, source/receipt corruption and ambient-module collisions. The exact committed read-only Git-free export passes replay and all 18 controls on CPython 3.13.16. All 19 publication-byte comparisons pass. Ruff, formatting and compilation checks pass.
  • Finite coverage includes all 4,097,782 five-/six-flats, 7,140 root planes, 960 reflections and complete A5 extension orbits. Internal mathematical and fresh artifact reviews found no remaining substantive objection. Evidence is author-checked; independent human and proof-kernel review remain separate.

Reproduce from the repository root:

RUN="$HOME/.cache/integer-mult-bounds-runs/a5-shortening-review"
mkdir -p "$RUN"
TMPDIR="$RUN" uv run --python 3.12 --no-project python -W error -B \
  scripts/research_package.py --package research/p112-a5-shortening

Merge Danger

Door: two-way

Blast Radius: isolated

Only the new research package changes. This closes one actual profile, not full C5, the complete decoder floor, a supplier or a new kappa. The standard Weyl-chamber theorem and original decoder reduction remain dependencies. The selected frontier and frozen inputs are unchanged; no full supplier cold replay, Lean or Docker build is claimed. Development used substantial automated drafting and finite checks.

@Mister-Meeseeks
Mister-Meeseeks merged commit 87866a0 into CrocSwap:main Oct 17, 2026
2 checks passed
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