§7 Exact strength: how the named theorems differ from the textbook

7. Exact strength: how the named theorems differ from the textbook

Mazur. Proved: irreducibility of $E_{P} [p]$ for Frey curves. Not proved: Mazur's theorems on rational isogenies or rational torsion for general curves. For $p \leq 13$ the argument is Kummer or descent, not modular curves.
Langlands–Tunnell. Proved: the octahedral case with explicit lift, for surjective $ρ ˉ_{3}$ with cyclotomic determinant, delivered as a weight-one form and then as weight-2 residual modularity with level conditions. Not proved: automorphy of general odd two-dimensional representations with soluble image.
Modularity lifting. Proved: the two level-conditioned statements of §4.2 for semistable $W$ at $p = 3$ and $p \in {3, 5}$ . Not proved: a statement without the conditions on $M_{0}$ , for non-semistable curves, or for other $p$ .
Wiles. Proved: every semistable integral Weierstrass model with $Δ \neq = 0$ is modular in the $a_{ℓ}$ -matching sense. The hypothesis is on a chosen integral equation; nothing is said about non-semistable curves, modular parametrisations or $L$ -functions.
Ribet. Proved: level lowering for the Frey representation at conductor-supported squarefree levels, in the congruence-of-traces formulation. Not proved: Ribet's theorem for a general modular mod- $p$ representation.
"Irreducible" is $F_{p}$ -irreducibility of $E [p]$ ; absolute irreducibility, where lifting needs it, is derived inside (ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd).