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.
Scope: Every compact convex cover universal for finite polygonal worms or for all unit worms has area strictly greater than 0.23743658226923856768, both with direct motions and when reflections are allowed.
Lean checkedRecorded build passed
Unfinished proof stepsNone
PublicationReview pending
Starting pointA universal convex cover
→
RelationMixed-area witnesses and calibrated angular bounds
→
ConclusionArea > 0.23743658226923856768
Exact scope: Every compact convex cover universal for finite polygonal worms or for all unit worms has area strictly greater than 0.23743658226923856768, both with direct motions and when reflections are allowed.
Main theorem
Direct-Motion Universal Worm Lower Bound
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.
The theorem dossier brings together the expanded exact proposition, complete checked source, and checker evidence.
The September 2 paper proves that both the direct and reflection-allowed convex-worm covering infima exceed 0.23743658226923856768, improving the prior 0.232239 lower bound. The exact optimum remains open. A separate Lean development checks stronger pointwise versions for each universal convex cover.
Author-authorized early release. This fixed paper package first appeared while independent presentation review was pending; hosting it does not mark the Lean result accepted.
Hosting authorized by the rightsholder. ProofAtlas metadata cover; not a reproduction of a paper page or part of the proof.
Lech Mazur, “A Mixed-Area Lower Bound for Moser's Convex Worm Problem,” September 2, 2026.
The four Lean endpoints are pointwise inequalities for each universal convex cover. The paper separately takes infima to state bounds for M_+ and M_±; that infimum packaging is not a Lean declaration in this release.
The source release ledger reports successful targeted checks, aggregate replay, no admissions, and the standard foundation closure propext, Classical.choice, and Quot.sound. ProofAtlas accepted-result status remains separate because the retained evidence is not the complete hash-bound build transcript required by the current contract.
The paper's adversarial audit predates the final 21:22 build. Its mathematical and expository findings F2–F5 are repaired in the matching final TeX; F1 is resolved by the permanent ProofAtlas routes published with this package.
Neither the paper nor the Lean result determines the exact optimal cover, establishes optimality of the lower bound, or closes Moser's convex worm problem.
Paper overview
Moser's convex worm problem and the improved lower bound
Author-supplied explanation of the covering problem and the new lower bound. The scaled interval shows about 18.1% of the previously open gap closed; the image is explanatory, not proof or formal-verification evidence.
Scope limits
What this formalization does not claim
The four formal endpoints are pointwise cover-area inequalities; the paper separately takes infima to state the bounds for M₊ and M±.
The result is a lower-bound improvement and does not determine the optimal cover or solve Moser's convex worm problem.
The explanatory infographic and adversarial manuscript audit are not Lean proof evidence.
The disclosed Lean foundations are standard logical foundations, not geometric assumptions.
Continue the mathematics
Open questions and extensions
Use the pinned Lean source to inspect the mixed-support packing theorem, calibrated angular partitions, finite midpoint worms, and the four pointwise endpoints. Further work can improve the bound or narrow the upper bound, but must preserve the exact motion mode, worm class, and distinction between pointwise cover inequalities and infimum packaging.
What the source ZIP contains
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
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.
Formal theorem review status — 4 questions open
Independent review
Four review questions remain open
Lean has checked the exact source, but ProofAtlas has not accepted this result. Independent AI, human, or mixed reviewers may examine the build evidence, statement alignment, result boundary, and public wording. Review does not replace Lean's check or broaden the theorem.
Review 1
Formal evidence
An independent reviewer must inspect the recorded build, declarations, unfinished-proof-step check, and disclosed foundations.
Review 2
Statement alignment
The formal declaration must be reviewed against the theorem wording and its exact variant.
Review 3
Result boundary
The limits must be checked so the page cannot imply a broader theorem.
Review 4
Public wording
The explanation, infographic labels, and source presentation need independent review.
Source
Canonical source
The permanent source link and downloadable files must be approved for public citation.
Final record
Accepted result
After the four reviews and source route are ready, an accepted-result record must bind them to this exact formalization.
Credit for this release
Contributors and roles
Authorship and other contributions are recorded separately for this version.
Authorship
Paper author
Lech Mazur
Contributions
Direct contributionOpenAI Codex, OpenAI GPT-5.6 Pro
OpenAI GPT-5.6 Pro and OpenAI Codex have source-reported roles in mathematical exploration, proof development, computational testing, adversarial auditing, formalization, and exposition.
Computation
Exposition
Formalization
Gap or error discovery
Proof strategy
Direct contributionLech Mazur
Lech Mazur is the paper author and accountable editor and directed the AI-assisted research, verification process, output selection, and reconciliation.
Exposition
Proof strategy
Research direction
Citation
Cite this release
Use the version-specific citation so the authorship, scope, and public record remain attached.
