Formalizing Fefferman's Official Periodic Navier-Stokes Problem (B) in Lean 4: Global Linear Strain Exclusion on T3, Biot-Savart Direction Depletion Identities, and Conditional Reductions via Beale-Kato-Majda

We present a self-contained Lean 4 formalization (leanprover/lean4:v4.30.0-rc1, Mathlib 4, 184 kernel-verified theorems across 5 modules with zero sorry and zero non-standard axioms outside [propext, Classical.choice, Quot.sound]) of Charles L. Fefferman's official periodic 3D incompressible Navier-Stokes problem statement (Statement (B) on R^3/Z^3) together with proved geometric/kinematic/ODE theorems and explicit conditional reductions to Clay_B_exact. Scientific Honesty & Scope Notice (Proved Theorems vs. Open Hypotheses): Unconditionally Proved Global Linear Strain Exclusion on T^3: We prove unconditionally that spatial Z^3-periodicity forces any global linear map on R^3 to vanish identically (z3_periodic_linear_eq_zero), excluding any non-zero global uniaxial linear Burgers background strain diag(-alpha/2, -alpha/2, alpha)x (burgersLinearStrain_not_z3_periodic). Crucially, torus periodicity rules out only a global linear background strain; localized Burgers-like vortex structures can still form locally on T^3, so this fact does NOT yield unconditional Clay (B). Unconditionally Proved Biot-Savart Direction-Alignment & ODE Comparison Theorems: We prove the pointwise Biot-Savart determinant cancellation on aligned vorticity (biot_savart_det_aligned_eq_zero, aligned_vorticity_stretching_integrand_zero, biot_savart_det_difference_identity), parabolic lambda^6 scaling homogeneity (navier_stokes_scaling_homogeneity_deg6), the non-vacuity and step-jump exclusion theorems for IsPhysicalNSSolution (stepField_not_physical, repaired_huniq_at_zero), and the first-exit-time ODE comparison ceiling M(t) <= max(M(0), C_CZ / kappa'') from M'(t) <= C_CZ M(t)^2 - kappa'' M(t)^3 (comparison_ode_ceiling). Conditional Reductions & Open Hypotheses: The theorems clay_B_exact_of_periodic_tether_bound and clay_B_exact_of_torus_direction_depletion are conditional reductions. Their analytic closure hypotheses (PeriodicDirectionDepletionBound, PeriodicTetherClosingBound, and PeriodicBKMContinuation) remain OPEN and are stated explicitly as hypotheses in the theorem signatures. Neither Clay (B) nor Clay (A) is claimed solved. GitHub Repository: https://github.com/BenFrohman/fefferman-clay-navier-stokes (Commit 9bd8a9675993cb973f66216de696b20f7c489b71, Release v1.0.0) Verification & Provenance: Audited with Titan Audit (DOI: 10.5281/zenodo.23630648), SealGuard (DOI: 10.5281/zenodo.23631670), and Sentinel Gate (DOI: 10.5281/zenodo.23632766).