Skip to content

v9.1.0 Real Formal Immersion Matrix - M3=[[1,1],[0,2]] Rank 2 mod 3 Decided + A+B Real

Choose a tag to compare

View all tags
@DavidFox998 DavidFox998 released this 02 Sep 01:23
v9.1.0
62fd5db

v9.1.0: Phase C Real Matrix Rank - Formal Immersion at 3 Decided

Phase C now carries real finite formal-immersion matrix evidence at 3. The explicit differential evaluation table over ZMod 3 computes M3 = [[1,1],[0,2]], with determinant 2 != 0 mod 3 and rank two proved by decide.

Real finite chain

  • Phase A: all 80 S-unit/quartic checks at p=2,13 pass; all eight candidates remain, so no singleton Selmer claim is made.
  • Phase B: S2(26) q-expansion tables, Hecke checks at 2 and 13, distinctness, and dimension-two evidence.
  • Phase C: degree-six hyperelliptic model, differential basis omega1=dx/y and omega2=x dx/y, four cusp reduction tokens, Abel-Jacobi replay rows, differential table, and the decided rank-two M3 certificate.

Verification

  • Focused builds for FormalImmersion_26, J0_26_Decomp, SecondDescent_Real_26, and ConditionalBealTheorem passed.
  • Full Lean build passed in GitHub Actions.
  • The finite matrix rank theorem introduces no axioms.
  • The combined transport/formal-immersion evidence uses only Lean foundations: propext, Classical.choice, Quot.sound.
  • No new sorry, admit, opaque proof placeholder, sorryAx, Lean.ofReduceBool, or native_decide was introduced.

Honest boundary

The actual Abel-Jacobi map, smooth reduction, geometric implication to the four-cusp classification, the Jacobian isogeny J0(26) ~ E26a1 x E26b1, modularity, and level-lowering remain explicit conditional data. This release does not claim an unconditional proof of Beal's Conjecture.

Implementation merge: 0a28f24
Release snapshot: 62fd5db
Validation PR: #16
Concept DOI: https://doi.org/10.5281/zenodo.22041831

Archive: beal-conjecture-v9.1.0.tar.gz
Size: 182665 bytes
SHA-256: 581c9f3ce63e1a379c6163749a16bff55d837c999f0f57af39f506ce727b7b89

DOI

Zenodo preserves the GitHub-hook source ZIP; its README and Phase A/B/C release-critical Lean files were verified byte-for-byte against the annotated v9.1.0 tag. The canonical attached tarball remains beal-conjecture-v9.1.0.tar.gz with the size and SHA-256 listed above.

Assets 3
Loading