Work in progress: A Lean 4 Formalization of the Classical Continuation Chain for Periodic Navier-Stokes on 𝕋³: Energy Identity, H³ Commutator Reduction and the BKM Route

Work in progress (draft). Companion paper to the Lean 4/Mathlib repository. Proved unconditionally: H^3 BKM control and the periodic BKM criterion. Clay Statement (B) is proven only conditionally on the open named Prop PeriodicBKMIntegrability. Does NOT solve the Clay problem or prove Navier-Stokes regularity. Source: https://github.com/BenFrohman/periodic-ns-classical-continuation at commit 767d55c. Sibling reduction paper: 10.5281/zenodo.23842296. © 2026 Benjamin Stanley Frohman (ORCID 0009-0006-7068-3718). Licensed under Apache-2.0. New version: corrected PDF (banner/DOI wording, updated status). Work in progress; does not solve the Clay problem. New version (v3): typeset with new LaTeX harness; claims unchanged. Work in progress; does not solve the Clay problem. New version (v4): adds the Oct 31 2026 bending-rate hidden-property hypothesis (open) and a proved breakdown of the Constantin-Fefferman step (algebraic depletion bound, L1 Gronwall); open steps remain named hypotheses. Work in progress; does not solve the Clay problem. New version: PeriodicH1TrilinearBound (Ladyzhenskaya-type estimate, explicit constant) and PeriodicMeanConservation now proved in Lean; small-data continuation depends only on the named PeriodicH1BlowupCriterion (not formalized). Work in progress; does not solve the Clay problem. New version (v6): Leray H1 blow-up criterion and the analytic Constantin-Fefferman/Beirão da Veiga-Berselli step broken into smaller named hypotheses with proved reductions (ClassicalSteps.lean); open steps remain named hypotheses. 720 theorems and lemmas, 0 sorry. Work in progress; does not solve the Clay problem. New version: v7: Lean-proved energy equality reducing PeriodicEnstrophyTimeIntegrable to a named nonlinear-cancellation Prop; standard H2 smoothing Props; flagged mismatch of the older pointwise H2 smoothing Prop. Work in progress; does not solve the Clay problem. New version: v8: academic copyedit of the paper (introduction, formal wording, LaTeX typesetting of all mathematics) and a stated theorem-counting convention (source count vs. kernel count). No mathematical claim or status changed; no Lean source changed. Work in progress; does not solve the Clay problem.