Mazur's rational torsion theorem

 Mazur's rational torsion theorem🔗

Compiled2026-08-01T13:15:26ZProject4d20ee3Port to Lean 4.33 and publish an interactive Verso roadmap (#17)Leanleanprover/lean4:v4.33.0-rc1VersoBlueprint51ebcae4b3133f407807e581178d2dcc705ac683@51ebcae4b313

This Blueprint is the canonical dependency map for the remaining formalization of Mazur's theorem. Its 48 labelled nodes are the exact work items from coordination/program.json. A uses arrow records a mathematical dependency; stage membership is shown by the six groups. Existing declarations are named as such, while every not-yet-built interface is explicitly marked proposed.

Contents

  1. 1. 01 — Integrated baseline
  2. 2. 02 — Finite-level endpoints
  3. 3. 03 — Shared algebraic geometry and isogenies
  4. 4. 04 — Prime-level infrastructure
  5. 5. 05 — Mazur's prime-order argument
  6. 6. 06 — Integration and hardening
  7. Dependency Graph
  8. Blueprint Summary