Prime torsion forces semistability. For a prime p\ge 17, finite-flat uniqueness and Néron-model specialization exclude additive reduction of an elliptic curve carrying a rational point of order p.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): MazurTorsion.PrimeOrder.primeTorsion_semistable Prove that a rational point of prime order p at least 17 forces semistable reduction.

Torsion specializes outside identity components. Hasse bounds and component groups place the marked point outside the identity component at 2, 3, and all bad primes.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): MazurTorsion.PrimeOrder.primeTorsion_specializesOutsideIdentity Use Hasse bounds and component groups to locate the marked point outside the relevant identity components.

Specialize through the Eisenstein quotient. Map the integral X_0(p) point to the Eisenstein quotient and compare its specializations in two residue characteristics.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): MazurTorsion.PrimeOrder.eisenstein_specialization_comparison Compare the two specializations of the integral modular point after mapping to the Eisenstein quotient.

The division-field extension is everywhere unramified. The comparison forces the relevant p-division extension over \mathbb{Q}(\zeta_p) to be unramified at every finite place.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): MazurTorsion.PrimeOrder.divisionField_everywhereUnramified Prove that the p-division field extension over the p-th cyclotomic field is everywhere unramified.

Exclude the inverse-cyclotomic extension. The Herbrand–Kummer calculation and B_2=1/6 rule out the unramified character extension demanded by the division field.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): MazurTorsion.PrimeOrder.inverseCyclotomic_extension_impossible Apply the Herbrand-Kummer calculation to rule out the required inverse-cyclotomic extension.

Split the p-torsion extension. Split 0\to\mathbb{Z}/p\mathbb{Z}\to E[p]\to\mu_p\to0 after the forbidden character extension has been excluded.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): MazurTorsion.PrimeOrder.primeTorsion_exactSequence_split Split the exact sequence from the rational p-torsion line to its cyclotomic quotient.

Shafarevich finiteness for the isogeny chain. Only finitely many rational elliptic curves up to isomorphism have good reduction outside a prescribed finite set, in the exact form consumed by quotient iteration.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): MazurTorsion.PrimeOrder.Shafarevich.finiteIsomorphismClasses Give the finiteness theorem for elliptic curves with a prescribed finite set of bad primes.

The infinite isogeny-chain contradiction. Iterate quotient isogenies by the split rational subgroup; Shafarevich finiteness contradicts the resulting infinite sequence, excluding rational prime order p\ge17.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): MazurTorsion.PrimeOrder.rationalPoint_addOrderOf_ne_prime_ge_seventeen Exclude every rational point of prime order p at least 17 by the quotient-isogeny chain contradiction.