Skip to content

v9.4.0: Formal immersion X0(26)->J0(26) at 2 via M3 rank 2

Choose a tag to compare

View all tags
@DavidFox998 DavidFox998 released this 02 Sep 16:00
· 23 commits to main since this release
v9.4.0
e665e0d

v9.4.0 — Formal immersion X0(26) -> J0(26) at 2 via M3 rank 2

This release adds a reproducible finite formal-immersion witness for the level-26 route.

Verification

  • Formal-immersion JSON witness passed
  • J0(26) JSON witness passed
  • Focused Lean build passed
  • Full CI passed
  • Axiom output uses only propext, Classical.choice, and Quot.sound

Formal boundary

The explicit proposition-valued premises are J0DecompositionSoundness_26, MwrankCertificateSoundness_26, and FormalImmersionSoundness_26; they are not global axioms.

The chain is: v9.2 rank 0 (Selmer = {1}) + v9.3 dim J0(26) = 2 = 1 + 1 isogeny + v9.4 M3 rank 2 => X0(26)(Q) finite.

Follow-up Task #495 records construction of the level-26 cotangent map behind the finite witness.

Assets 7
Loading