Skip to content

v10.0.0: ConditionalBealTheorem — Opera Numerorum — explicit premises

Choose a tag to compare

View all tags
@DavidFox998 DavidFox998 released this 02 Sep 16:37
· 17 commits to main since this release
v10.0.0
dabb9f1

Focused build Beal.Final.ConditionalBealTheorem passed, Axiom only [propext, Classical.choice, Quot.sound], No new axiom/sorry/admit/True stubs. Premises: J0DecompositionSoundness_26, MwrankCertificateSoundness_26, FormalImmersionSoundness_26, FreyCurveExists (reuses FreyCurveConstruction_26), LevelLowering_26 (packages indexed modularity supplier + LevelLoweringCertificate_26). Chain v9.2+v9.3+v9.4+v10. Task #495 remains v10.0.1 hardening for explicit cotangent map M3.

Assets 6
Loading