Bulk Velocity Vanishes (Section 6)

Proves that the drift velocity u_inf = 0 using Ampere's law, Stokes' theorem on the torus, and positivity of the charge density.

theorem VML.dotProduct_smul_self (c : ℝ) (v : Fin 3 → ℝ) : v ⬝ᵥ c • v = c * normSq v

Helper: dotProduct with scalar multiplication

theorem VML.bulk_velocity_zero {X : Type u_1} [FlatTorus3 X] (ss : VMLSteadyState X) : ss.b₀ = 0

Lemma 19: The drift velocity vanishes: u∞ = 0. Reference: lem:u_zero

Proof: From Ampère (∇×B = J = ρ u∞) and ∫ u∞ · ∇×B dx = 0 (Stokes), we get |u∞|² ∫ ρ dx = 0. Since ∫ ρ > 0, u∞ = 0.