Work in progress: A Lean-verified conditional reduction of periodic Navier-Stokes regularity on T^3 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 0cd3551. © 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.