the telescoping chain from the later start to the terminal level("Multiplying just the

lower inequalities in (9), or using ∏(1-e_j) ≥ 1 - ∑ e_j, gives a_M ≥ a_{j*}/2"). Uses only conjunct (ii) of the Step-down body Integration.IndyStepDownStatement, the later scale condition later_scale_of_le, and the construction of the T iterates exists_TIterates.

theorem AVenhance.Infra.Section5.RelativeError.kappaSeq_pos_of_ge {β C₀ : ℝ} (hβ1 : 1 < β) (hb : β < 4 / 3) (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hx : I.Cxi ≤ C₀) (hh : I.Chat ≤ C₀) {κ : ℝ} (hκp : κ ∈ permissibleSet β I.Λ) {M : ℕ} (hM : 1 ≤ M) (hperm : κ ∈ permittedInterval β I.Λ M) {j k : ℕ} (hj1 : 1 ≤ j) (hjM : j < M) (hjk : j ≤ k) (hkM : k ≤ M) : 0 < I.kappaSeq κ M k

The coarse diffusivities κ_k are positive for j ≤ k ≤ M once 1 ≤ j < M.

theorem AVenhance.Infra.Section5.RelativeError.chain_lower_bound (β C₀ : ℝ) (hβ : 6 / 5 ≤ β) (hA8 : Integration.IndyStepDownStatement β C₀) : ∃ (Λ₀ : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λ₀ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → (∀ (j : ℕ), ClassicalSolvable (streamVel (Φ j))) → ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (R : ℝ), 0 < R → laterStart β I.Λ R < M → ∀ (g : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) g → IsZ2Periodic g → Homogenization.MeanZeroOn unitCube g → IsThetaAnalytic R g → ∃ (θj : ℝ → Homogenization.Vec 2 → ℝ) (θM : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (laterStart β I.Λ R))) (I.kappaSeq κ M (laterStart β I.Λ R)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θj ∧ IsClassicalSol (streamVel (Φ M)) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θM ∧ (I.kappaSeq κ M (laterStart β I.Λ R) * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θj t) x) ≤ 2 * (κ * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θM t) x)

Item 13, chain step: below a Λ-threshold, for a classical solution at every level j* ≤ k ≤ M (j* = laterStart β Λ R < M), the dissipation at the later start is at most twice the terminal dissipation.