Lean Dependency Graph

A zoomed-in view of how the 46 files in ManifoldProofs/ depend on each other.

Top-level structure

Verification metadata

• Lean 4.28.0 + Mathlib v4.28.0
• Zero sorry statements across all 46 files
• Zero custom axioms. The artifact relies on Lean's three standard axioms only: propext, Classical.choice, Quot.sound.
• lake build succeeds with no errors.

Re-running the verification

cd ManifoldProofs
lake build

This builds all 46 files; expect a few minutes on a warm Mathlib cache. MoF_FinalVerification cross-checks that the master theorem depends on exactly the stated axioms.

Which files depend on MoF_08_DefenseBarriers

MoF_08 is the continuous-case core. Everything downstream either imports it directly or depends on something that does.

Where to start reading Lean

• First-time reader: MoF_08_DefenseBarriers — eight theorems, ~200 lines, every proof is directly readable.
• Quantitative tier: MoF_11_EpsilonRobust — Lipschitz bound + positive-measure band.
• Discrete tier: MoF_12_Discrete — finite-set counting.
• Unified view: MoF_14_MetaTheorem — the two-line master argument.
• Capstone: MoF_MasterTheorem — the packaged version used in the paper.