Fourier Lemmas on the Three-Torus: Heat Smoothing, the L2 Strain Identity, and the Curl of the Energy Derivative, Formalised in Lean 4

Lean 4 formalisation on T^3 of the heat semigroup and Sobolev smoothing, the L2 strain identity ||S||^2 = 1/2 ||omega||^2, the energy functional derivative and Biot-Savart curl, and finite-mode Galerkin results (local existence, structure preservation, H^s transport bound for s>5/2, uniform short-time bound, tame Gronwall propagation, continuation under an a priori bound). Build: 14 modules, 250 theorems, 0 nonstandard axioms. Proved: kernel-checked Lean 4 + Mathlib theorems, no sorry, only standard axioms (propext, Classical.choice, Quot.sound), per #print axioms and AXIOMS.md. Conditional results are stated with their hypotheses as explicit named Props. This work does not solve the Clay Millennium problem; global regularity of 3D Navier-Stokes remains open. Files: paper PDF and the GitHub source tarball of the archived commit.