Lorentz Force Component Bound

Proves lorentz_component_bound: each component of the Lorentz force (E + v x B) is bounded by C * (1 + ||v||). Used by CoulombSpatialTransport for bounding spatial transport integrands.

theorem VML.lorentz_component_bound (E₀ B₀ : Fin 3 → ℝ) : ∃ (CL : ℝ), 0 ≤ CL ∧ ∀ (v : Fin 3 → ℝ) (i : Fin 3), |(E₀ + cross v B₀) i| ≤ CL * (1 + ‖v‖)

Bound on a Lorentz force component: |(E₀ + v × B₀)ᵢ| ≤ C·(1 + ‖v‖). Each cross product component is bilinear in v, B₀, hence linear in ‖v‖. Proved by Aristotle.