Mazur's rational torsion theorem

1. 01 — Integrated baseline🔗

Theorem1.1
uses 0
Used by 13
Reverse dependency previews
Preview
Theorem 2.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
XL∃∀N
EffortlargePriorityhighTagsmilestonedoneintegratedmazur

Imported sorry-free Mazur baseline. The compiled baseline supplies the finite-group classification and cardinality assembly; the full 2-, 3-, 4-, 5-, and 7-torsion obstructions; exceptional products; and unconditional exclusions of orders 14, 15, 16, 20, 21, 24, and 27.

Status: done.

Canonical deliverables — these names are authoritative for this node:

  • definition (integrated): MazurTorsion.RationalTorsion The rational torsion subgroup on which the point-order and cardinality reductions are stated.

  • definition (integrated): MazurTorsion.cyclicOrders The finite set of cyclic point orders allowed by the target classification.

  • definition (integrated): MazurTorsion.remainingKubertForbiddenOrders The exact residual composite-order callbacks exposed by the imported baseline.

  • theorem (integrated): MazurTorsion.rationalTorsion_orders_mem_cyclicOrders_of_remaining_obstructions The checked point-order reduction from the remaining prime and composite exclusions.

  • theorem (integrated): MazurTorsion.torsion_ncard_le_of_explicit_arithmetic The checked cardinality bound once the explicit point-order hypotheses are supplied.

Proof for Theorem 1.1
uses 0

The repository imports the pinned Clawristotle corpus, removes every sorry, and kernel-checks the resulting modules under the project axiom policy. The remaining callbacks are deliberately exposed by the downstream nodes rather than hidden in this milestone.