Conditional infrastructure for conjunct (i) of step-down estimate. The step-down estimate and big-bound estimate statement modules are intentionally not imported. Their source-scale estimates, the corrected initial-data estimate, and the classical forced-energy estimate enter as separate hypotheses below.

theorem AVenhance.Infra.Section5.IndyStepDownPartI.transfer_add {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : Heat.frozenCellToTorusL2 ⋯ = Heat.frozenCellToTorusL2 hf + Heat.frozenCellToTorusL2 hg

theorem AVenhance.Infra.Section5.IndyStepDownPartI.transfer_norm {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : ‖Heat.frozenCellToTorusL2 hf‖ = √(l2NormSq f)

theorem AVenhance.Infra.Section5.sqrt_l2NormSq_add_le {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : √(l2NormSq fun (x : Homogenization.Vec 2) => f x + g x) ≤ √(l2NormSq f) + √(l2NormSq g)

Minkowski's inequality in the actual cell L2 carrier.

theorem AVenhance.Infra.Section5.indyStepDown_part_i_conditional {β : ℝ} (I : Ingredients β) (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ I.Λ) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (m M : ℕ) (κ : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hκm : 0 < I.kappaSeq κ M m) (_hT : I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T) (C₇ Cᵢ Cₐ Cₜ Cenergy : ℝ) (hC₇ : 0 ≤ C₇) (hCenergy : 0 ≤ Cenergy) (hU : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => θm t x - I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x) (hAT : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x - T (Nstar β) t x) (hTP : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => T (Nstar β) t x - θprev t x) (hAP : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x - θprev t x) (hA7 : (timeHMinusOneNorm fun (t : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel (Φ m)) (I.kappaSeq κ M m) (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β))) t x) ≤ ENNReal.ofReal (C₇ * epsilon β I.Λ (m - 1) ^ delta β * √(I.kappaSeq κ M m) * √(l2NormSq θ₀))) (hInitial : √(l2NormSq fun (x : Homogenization.Vec 2) => θm 0 x - I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) 0 x) ≤ Cᵢ * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)) (hEnergy : ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x) + √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θm s) x - spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s) x) ≤ Cenergy * (√(l2NormSq fun (x : Homogenization.Vec 2) => θm 0 x - I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) 0 x) + (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel (Φ m)) (I.kappaSeq κ M m) (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β))) s x).toReal / √(I.kappaSeq κ M m))) (hSectionFourAnsatz : ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x - T (Nstar β) t x) ≤ Cₐ * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)) (hSectionFourIterate : ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => T (Nstar β) t x - θprev t x) ≤ Cₜ * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)) : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - θprev t x) + √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θm s) x - spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s) x) ≤ C * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)

Conjunct (i) of step-down estimate, conditional on the independently sourced big-bound estimate, Section 4 approximation, initial-defect, and classical energy estimates.

hA7 is the real source-scale form of the big-bound estimate assembly bound. hEnergy is the forced energy estimate for the actual difference theta_m - theta_tilde_m; its right side uses only that difference's initial datum and the normalized negative norm of the ansatz residual. hInitial is the aggregate initial defect bound at scale epsilon^delta. The identity below gives epsilon^(4 delta) for the oscillatory corrector contribution; the separate H_m term in e.Hm.Linfty is only controlled at epsilon^delta. The two Section 4 inputs are the L2 bounds corresponding to e.tildethetam.to.Tm and e.Tm.thetam. No step-down estimate conclusion is assumed.