The zero-amplitude branch, before any normalization by ‖θ₀‖₂.

theorem AVenhance.Infra.Section4.ThetaZeroBounds.theta_zero_word_eq {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hκ : 0 < κ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) (fun (x : Homogenization.Vec 2) => 0) θ) (w : List (Fin 2)) {t : ℝ} (ht : 0 ≤ t) : classicalWordDerivative w (θ t) = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section4.theta_zero_word_spatial_energy_eq_zero {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hκ : 0 < κ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) (fun (x : Homogenization.Vec 2) => 0) θ) (w : List (Fin 2)) {t : ℝ} (ht : 0 ≤ t) : thetaWordSpatialEnergy θ w t = 0

theorem AVenhance.Infra.Section4.theta_zero_word_spacetime_gradient_energy_eq_zero {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hκ : 0 < κ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) (fun (x : Homogenization.Vec 2) => 0) θ) (w : List (Fin 2)) : thetaWordSpaceTimeGradientEnergy θ w = 0

theorem AVenhance.Infra.Section4.theta_zero_energy_level_eq_zero {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (n : ℕ) (hφ : IsAdmissibleStream φ) (hκ : 0 < κ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) (fun (x : Homogenization.Vec 2) => 0) θ) : thetaEnergyLevel θ κ n = 0