Immutable source snapshot
Moser's Convex Worm Mixed-Area Lower Bound source at c9254797b42c
This permanent route identifies the exact Git snapshot used by the recorded Lean theorem. The complete checked import closure, source footprint, downloads, and checker evidence are available on the source page.
Git commitc9254797b42c2a89acb00281c0822c7d6fc21923
Recorded theorem endpoint
MoserWorm.directUniversal_area_ge_THat · MoserWorm.directUniversal_area_gt_published · MoserWorm.polygonalDirect_area_ge_THat · MoserWorm.polygonalDirect_area_gt_published · MoserWorm.polygonalReflection_area_ge_THat · MoserWorm.polygonalReflection_area_gt_published · MoserWorm.reflectionUniversal_area_ge_THat · MoserWorm.reflectionUniversal_area_gt_published
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.