Exact strength of the named steps
- Mazur. Proved: irreducibility of E_P[p] for Frey curves (p ≥ 17 by the Eisenstein quotient; p ≤ 13 by Kummer or descent, not modular curves). …
- Langlands-Tunnell. Proved: the octahedral case with explicit lift, for surjective ρ̄₃ with cyclotomic determinant, delivered as a weight-one form and then as weight-2 residual modularity with level conditions. …
- Modularity lifting. Proved: the two level-conditioned statements above for semistable W at p = 3 and p ∈ {3, 5}. …
- Wiles. Proved: every semistable integral Weierstrass model with Δ ≠ 0 is modular in the a_ℓ-matching sense. …
- Ribet. Proved: level lowering for the Frey representation at squarefree conductor-supported levels, as a congruence of traces. …
- "Irreducible" is F_p-irreducibility of E[p]; absolute irreducibility, where lifting needs it, is derived in the tree (
ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd).
Quoted from the section “Exact strength of the named steps” of PROOF-PATH.md of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: each “Proved:” clause, cut with … where the text goes on, and entries that say neither what is proved nor what is not, whole.
No landmark is placed in this section. The landmarks it names, placed in the steps:
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.