Hm flux identities and source bridges used by the positive-time pairing assembler.

theorem AVenhance.Infra.Section4.sourceErrorD_eq_dmFrozenSource {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) : (fun (z : ℝ × Homogenization.Vec 2) => Section5.sourceErrorD I hΦ m κ T z.1 z.2) = dmFrozenSource I hΦ m κ T fun (z : ℝ × Homogenization.Vec 2) => hmFrozenDFirstFlux I hΦ m κ T z.1 z.2

The sourceErrorD vector field is definitionally the d_m source split used by the Section 4 scale estimate.

theorem AVenhance.Infra.Section4.sourceErrorD_eLpNorm_le_of_dmFrozenSource {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {B : ℝ} (hsource : MeasureTheory.eLpNorm (dmFrozenSource I hΦ m κ T fun (z : ℝ × Homogenization.Vec 2) => hmFrozenDFirstFlux I hΦ m κ T z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal B) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => Section5.sourceErrorD I hΦ m κ T z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal B

Convert the finite source estimate into the exact d_m field used by the moving-flow pairing FTC.