First-party checked source

Source for Moser's Convex Worm Mixed-Area Lower Bound

This pinned Lean source formalizes the following mathematical result: Four Lean-checked pointwise area inequalities cover finite polygonal worms and all unit worms, with direct motions or reflections allowed. Their strict rational corollaries give the lower bound 0.23743658226923856768; the exact optimum remains open. Download the complete checked closure, open the endpoint, or browse its supporting modules to study the proof or develop an extension.

Read the theorem overview Complete checked Lean source · 72 Lean files · 4 evidence records · Download ZIP Open Main.lean

Immutable source commit: c9254797b42c2a89acb00281c0822c7d6fc21923

Each ZIP contains the checked first-party local Lean import closure, exact statements and boundaries, license, notice, evidence, a source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled; this is not a portable whole-repository release.

Proof and source

What is checked—and how much source supports it

Browse the counted source

Declarations covered by evidence: 8
First-party Lean files: 72
Lean source lines: 16,269
Main recorded file: 71 lines

How the source is counted

Line counts exclude blank lines; comments and documentation count. The total is the deduplicated, commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded. Declaration count means names covered by the artifact's recorded evidence, not every declaration in the source. Source footprint is not a difficulty or proof-quality score.

Exact theorem evidence

Direct-Motion Universal Worm Lower Bound

MoserWorm.directUniversal_area_ge_THat, MoserWorm.directUniversal_area_gt_published

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit: c9254797b42c2a89acb00281c0822c7d6fc21923
Main Lean file: MoserWorm/Assembly/Main.lean
Main-file footprint: 71 lines
File SHA-256: sha256:2f873beecb35c02bf40af8516eaef6393bb34533d9271e79eb8085b76c1e263f
Complete Lean closure: 72 files · 16,269 lines
Toolchain: leanprover/lean4:v4.30.0-rc2

Open main Lean file Download main Lean file Download checker evidence (JSON)Download Apache-2.0 license Download Lech Mazur notice

Exact theorem evidence

Polygonal Direct-Motion Worm Lower Bound

MoserWorm.polygonalDirect_area_ge_THat, MoserWorm.polygonalDirect_area_gt_published

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit: c9254797b42c2a89acb00281c0822c7d6fc21923
Main Lean file: MoserWorm/Assembly/Main.lean
Main-file footprint: 71 lines
File SHA-256: sha256:2f873beecb35c02bf40af8516eaef6393bb34533d9271e79eb8085b76c1e263f
Complete Lean closure: 72 files · 16,269 lines
Toolchain: leanprover/lean4:v4.30.0-rc2

Open main Lean file Download main Lean file Download checker evidence (JSON)Download Apache-2.0 license Download Lech Mazur notice

Exact theorem evidence

Polygonal Reflection-Allowed Worm Lower Bound

MoserWorm.polygonalReflection_area_ge_THat, MoserWorm.polygonalReflection_area_gt_published

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit: c9254797b42c2a89acb00281c0822c7d6fc21923
Main Lean file: MoserWorm/Assembly/Main.lean
Main-file footprint: 71 lines
File SHA-256: sha256:2f873beecb35c02bf40af8516eaef6393bb34533d9271e79eb8085b76c1e263f
Complete Lean closure: 72 files · 16,269 lines
Toolchain: leanprover/lean4:v4.30.0-rc2

Open main Lean file Download main Lean file Download checker evidence (JSON)Download Apache-2.0 license Download Lech Mazur notice

Exact theorem evidence

Reflection-Allowed Universal Worm Lower Bound

MoserWorm.reflectionUniversal_area_ge_THat, MoserWorm.reflectionUniversal_area_gt_published

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit: c9254797b42c2a89acb00281c0822c7d6fc21923
Main Lean file: MoserWorm/Assembly/Main.lean
Main-file footprint: 71 lines
File SHA-256: sha256:2f873beecb35c02bf40af8516eaef6393bb34533d9271e79eb8085b76c1e263f
Complete Lean closure: 72 files · 16,269 lines
Toolchain: leanprover/lean4:v4.30.0-rc2

Open main Lean file Download main Lean file Download checker evidence (JSON)Download Apache-2.0 license Download Lech Mazur notice

Deduplicated checked source

Complete Lean import closure

These exact bytes are shared by 4 theorem evidence records above, so the file browser is shown once.

Complete checked Lean closure

72 Lean files are available here

Start with the principal theorem and proof-architecture files below, or search the complete commit-pinned closure.

72Lean files

Search and browse all 72 checked Lean files

Every listed file is read from the same pinned Git commit. File links open raw source in a new tab; use the ZIP download for the complete package. External Mathlib modules are dependency-locked but are not copied into this first-party source tree.

Filter all 72 Lean files

Showing all 72 files

MoserWorm/Analysis28 files · 7,084 lines

MoserWorm/Analysis/FirstSlab.lean293 lines
MoserWorm/Analysis/FirstSlabBroadGap.lean368 lines
MoserWorm/Analysis/FirstSlabCusp.lean280 lines
MoserWorm/Analysis/FirstSlabCuspEndpoints.lean481 lines
MoserWorm/Analysis/FirstSlabCuspOuter.lean180 lines
MoserWorm/Analysis/FirstSlabIntegrals.lean136 lines
MoserWorm/Analysis/FirstSlabOpposite.lean378 lines
MoserWorm/Analysis/FirstSlabOppositeEdges.lean151 lines
MoserWorm/Analysis/FirstSlabOppositeEndpoints.lean331 lines
MoserWorm/Analysis/FirstSlabOppositeExtended.lean258 lines
MoserWorm/Analysis/FirstSlabOppositeRegion.lean201 lines
MoserWorm/Analysis/FirstSlabQPayoff.lean187 lines
MoserWorm/Analysis/FirstSlabReflectedBroadGap.lean361 lines
MoserWorm/Analysis/FirstSlabReflectedCusp.lean368 lines
MoserWorm/Analysis/FirstSlabSide.lean360 lines
MoserWorm/Analysis/FirstSlabSideLeft.lean317 lines
MoserWorm/Analysis/IntermediateAnalytic.lean131 lines
MoserWorm/Analysis/IntermediateBranches.lean155 lines
MoserWorm/Analysis/IntermediateCoarse.lean166 lines
MoserWorm/Analysis/IntermediateEndpoints.lean241 lines
MoserWorm/Analysis/IntermediateEnvelopes.lean293 lines
MoserWorm/Analysis/IntermediateL2Branches.lean112 lines
MoserWorm/Analysis/IntermediateL4Branches.lean149 lines
MoserWorm/Analysis/IntermediatePartition.lean252 lines
MoserWorm/Analysis/IntermediateResidualBasic.lean237 lines
MoserWorm/Analysis/IntermediateResidualRemaining.lean353 lines
MoserWorm/Analysis/IntermediateShiftedBranches.lean178 lines
MoserWorm/Analysis/SinusoidalInterpolation.lean167 lines

MoserWorm/Assembly3 files · 352 lines

MoserWorm/Assembly/Main.lean71 lines
MoserWorm/Assembly/Intermediate.lean92 lines
MoserWorm/Assembly/LargeAngle.lean189 lines

MoserWorm/Atomic6 files · 1,518 lines

MoserWorm/Atomic/Achirality.lean70 lines
MoserWorm/Atomic/Boundary.lean123 lines
MoserWorm/Atomic/Data.lean120 lines
MoserWorm/Atomic/Master.lean421 lines
MoserWorm/Atomic/PositiveBoundary.lean232 lines
MoserWorm/Atomic/Support.lean552 lines

MoserWorm/Basic2 files · 358 lines

MoserWorm/Basic/Plane.lean128 lines
MoserWorm/Basic/RigidPlacement.lean230 lines

MoserWorm/Calibration6 files · 1,178 lines

MoserWorm/Calibration/CertifiedSigns.lean544 lines
MoserWorm/Calibration/Comparisons.lean50 lines
MoserWorm/Calibration/Definitions.lean165 lines
MoserWorm/Calibration/IntervalArithmetic.lean173 lines
MoserWorm/Calibration/TaylorBounds.lean187 lines
MoserWorm/Calibration/TrigReduction.lean59 lines

MoserWorm/Geometry3 files · 450 lines

MoserWorm/Geometry/ConvexCover.lean80 lines
MoserWorm/Geometry/Polyline.lean90 lines
MoserWorm/Geometry/UniversalCover.lean280 lines

MoserWorm/Midpoint4 files · 702 lines

MoserWorm/Midpoint/Atomic.lean234 lines
MoserWorm/Midpoint/Data.lean181 lines
MoserWorm/Midpoint/Error.lean207 lines
MoserWorm/Midpoint/MovingAngle.lean80 lines

MoserWorm/Payoff4 files · 1,043 lines

MoserWorm/Payoff/Continuous.lean87 lines
MoserWorm/Payoff/Definitions.lean199 lines
MoserWorm/Payoff/Lipschitz.lean154 lines
MoserWorm/Payoff/Semantics.lean603 lines

MoserWorm/Polygon10 files · 1,331 lines

MoserWorm/Polygon/AffineNull.lean40 lines
MoserWorm/Polygon/FiniteEnvelope.lean169 lines
MoserWorm/Polygon/FiniteHull.lean126 lines
MoserWorm/Polygon/JointHull.lean54 lines
MoserWorm/Polygon/MixedSupport.lean103 lines
MoserWorm/Polygon/PackingSeparators.lean302 lines
MoserWorm/Polygon/PositiveBoundary.lean60 lines
MoserWorm/Polygon/PositiveBoundaryMotion.lean165 lines
MoserWorm/Polygon/SupportCap.lean76 lines
MoserWorm/Polygon/TriangleArea.lean236 lines

MoserWorm/Witness6 files · 2,253 lines

MoserWorm/Witness/AngleNormalization.lean244 lines
MoserWorm/Witness/CoverNormalization.lean368 lines
MoserWorm/Witness/Equilateral.lean457 lines
MoserWorm/Witness/LargeAngle.lean152 lines
MoserWorm/Witness/OneCap.lean503 lines
MoserWorm/Witness/UniversalAdmission.lean529 lines

Source hashMatches checked record

Lean buildPassed in recorded evidence

LicenseApache-2.0 · Lech Mazur

Provenance and reproducibility

Exact checked source, with reuse terms

The endpoint and every listed local import come from the exact recorded Git commit, and the endpoint matches the stored source hash byte for byte. The locally authored package material is licensed under Apache-2.0 by Lech Mazur; Mathlib and cited third-party material remain under their own terms. Machine-readable checker evidence is included.