Work in progress: A Lean-verified conditional reduction of periodic Navier-Stokes regularity on 𝕋³ to a single integrability hypothesis

Work in progress (draft). Lean 4/Mathlib formalization. Proved unconditionally: H^3 BKM control (periodicBKMHsControl_three) and the periodic BKM criterion (periodicBKMCriterion). Proved conditionally on the named Prop PeriodicBKMIntegrability (open; equivalent in difficulty to Clay Statement (B)): Clay_B_exact via clay_B_exact_of_integrability. Does NOT solve the Clay problem or prove Navier-Stokes regularity. Source: https://github.com/BenFrohman/periodic-ns-classical-continuation at commit a5bf622. © 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.