Time integration of the actual classical energy pairing, including t = 0. FTC is applied on the open time interval, so no two-sided derivative at the initial boundary is imposed.

theorem AVenhance.Infra.Section4.IteratesTime.time_cell_integrable {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f unitCube MeasureTheory.volume

theorem AVenhance.Infra.Section4.iterate_smooth_time_energy_pairing {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) {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))) : ∫ (s : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, u s x * deriv (fun (t : ℝ) => u t x) s = (l2NormSq (u T) - l2NormSq (u 0)) / 2

FTC and Fubini turn the actual time pairing into the energy difference. The integrability premise is on the actual pairing, not an energy bound.

theorem AVenhance.Infra.Section4.iterate_classical_time_energy_pairing {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ 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))) : ∫ (s : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, u s x * deriv (fun (t : ℝ) => u t x) s = (l2NormSq (u T) - l2NormSq u₀) / 2

Specialize time FTC to the actual classical initial trace.

theorem AVenhance.Infra.Section4.iterate_material_time_square_pairing {φ u : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hu : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => u p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (hsmooth : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (u t)) (hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t)) {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))) : ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, u t x * amnrMaterial (streamVel φ) u t x = (l2NormSq (u T) - l2NormSq (u 0)) / 2

The transported half-square identity on the periodic cell. Drift cancels by spatial transport IBP; only positive-time derivatives are used. The joint regularity premise is C1, allowing the finite-regularity memory primitive.