Exact terminal-time energy of actual differentiated increments. The drift commutator and differentiated forcing retain their signed pairings.

theorem AVenhance.Infra.Section4.iterate_scalar_forced_time_energy_identity {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ F u₀ u) {T : ℝ} (hT : 0 ≤ T) (hI : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => u p.1 p.2 * deriv (fun (s : ℝ) => u s p.2) p.1) ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube))) (hG : IntervalIntegrable (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (u t) x)) MeasureTheory.volume 0 T) : (l2NormSq (u T) - l2NormSq u₀) / 2 + κ * ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (u t) x) = ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, u t x * F t x

Terminal-time energy identity for actual scalar forcing. Spatial forcing regularity is derived from the classical equation and admissible stream.

theorem AVenhance.Infra.Section4.iterate_classical_word_time_energy_identity {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ F u₀ u) (w : List (Fin 2)) {T : ℝ} (hT : 0 ≤ T) (hI : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => iterateSpatialWord w (u p.1) p.2 * deriv (fun (s : ℝ) => iterateSpatialWord w (u s) p.2) p.1) ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube))) (hG : IntervalIntegrable (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (u t)) x)) MeasureTheory.volume 0 T) : (l2NormSq (iterateSpatialWord w (u T)) - l2NormSq (iterateSpatialWord w u₀)) / 2 + κ * ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (u t)) x) = ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, iterateSpatialWord w (u t) x * (iterateSpatialWord w (F t) x - iterateWordMaterialError (fun (z : AmnrSpace) => streamVel φ z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x))

Apply exact terminal-time energy to the actual spatial word. The right side contains the differentiated original forcing minus the expanded drift error, with the initial word trace retained. No energy recurrence is assumed.

theorem AVenhance.Infra.Section4.iterateSpatialWord_zero (w : List (Fin 2)) : (iterateSpatialWord w fun (x : Homogenization.Vec 2) => 0) = fun (x : Homogenization.Vec 2) => 0

Spatial words of zero initial data are identically zero.

theorem AVenhance.Infra.Section4.iterate_classical_word_time_energy_identity_of_smooth {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} {F : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ F u₀ u) (w : List (Fin 2)) {T : ℝ} (hT : 0 ≤ T) : (l2NormSq (iterateSpatialWord w (u T)) - l2NormSq (iterateSpatialWord w u₀)) / 2 + κ * ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (u t)) x) = ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, iterateSpatialWord w (u t) x * (iterateSpatialWord w (F t) x - iterateWordMaterialError (fun (z : AmnrSpace) => streamVel φ z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x))

The actual smooth carrier supplies both natural integrability premises of the all-order terminal-time energy identity.