Scalar assembly facts for the main theorem. Energy is an explicit input, not a claim that weak-solution energy has been . Nonzero energy is distinguished from pointwise nonzero representatives in the analytic-radius bridge.

theorem AVenhance.Infra.Section5.energy_dissipation_bound_conditional {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} {Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (henergy : ∀ t ∈ Set.Icc 0 1, l2NormSq (θ t) + 2 * κ * ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 t ×ˢ unitCube, Homogenization.vecNormSq (Dθ p.1 p.2) = l2NormSq θ₀) : κ * spaceTimeGradNormSq Dθ ≤ l2NormSq θ₀ / 2

Literal energy balance, evaluated at t=1. Its space-time integral is over (0,t)×unitCube, the same carrier as the dissipation at t=1. The weak solution and drift hypotheses are unnecessary once this identity is supplied.

theorem AVenhance.Infra.Section5.analytic_gradient_bound {f : Homogenization.Vec 2 → ℝ} {R : ℝ} (hf : ContDiff ℝ 1 f) (ha : IsThetaAnalytic R f) : gradNormSq (spaceGrad f) ≤ 2 * l2NormSq f / R ^ 2

The n=1 analytic estimates bound the Euclidean gradient, with its two coordinate directions retained.

theorem AVenhance.Infra.Section5.analytic_radius_bound {f : Homogenization.Vec 2 → ℝ} {R : ℝ} (hf : ContDiff ℝ 1 f) (hp : IsZ2Periodic f) (hm : ∫ (x : Homogenization.Vec 2) in unitCube, f x = 0) (hA : 0 < l2NormSq f) (hR : 0 < R) (ha : IsThetaAnalytic R f) : R ≤ 1 / (√2 * Real.pi)

for smooth, mean-zero data of positive L2 energy. Pointwise nonzero alone is not a nonzero L2 class in the carriers.