Skip to content

v8.8.0 — Conditional Phase D Level-26 Frey Endgame

Choose a tag to compare

View all tags
@DavidFox998 DavidFox998 released this 01 Sep 17:03
v8.8.0
881926a

Conditional Phase D — level-26 Frey endgame

This release archives the green GitHub main commit 881926ae90341b60bbaf8254475ad9c8fa7fd6a4.

Added

  • lean/Beal/Mazur/Frey/LevelLowering_26.lean
  • A proof-relevant conditional interface connecting a primitive Beal counterexample to a noncuspidal rational point on the displayed level-26 model.
  • Explicit supplier boundaries for Frey construction, modularity and R=T, level lowering, second descent, Jacobian transport, and formal immersion.
  • The final contradiction after the existing Phase A–C rank-zero and four-cusp certificates.

Formal status

This is a conditional formalization milestone, not an unconditional Lean proof of Beal’s conjecture. The new principal theorems compile with no sorryAx and depend only on Lean’s standard {propext, Classical.choice, Quot.sound} foundations. No executable sorry, admit, axiom, opaque, or Boolean proof stub was introduced.

The release does not claim that the modularity, level-lowering, Frey-construction, or displayed-model interpretation boundaries have been proved in Mathlib 4.12.

Verification

Assets 2
Loading