Conditional relative-step assembly with constants chosen before Ingredients. The named physical leaves are ordinary hypotheses. This module never imports Big-bound estimate or step-down estimate and does not certify their unresolved physical inputs.

theorem AVenhance.Infra.Section5.RelativeError.relative_step (β C₀ A Ci Cr Ca Ct : ℝ) (hA : 2 ^ 14 ≤ A) (hCi : 0 ≤ Ci) (hCr : 0 ≤ Cr) (hCa : 0 ≤ Ca) (hCt : 0 ≤ Ct) : ∃ (C : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (R : ℝ), 0 < R → ∀ (g : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) g → IsZ2Periodic g → Homogenization.MeanZeroOn unitCube g → IsThetaAnalytic R g → ∀ (m : ℕ), mTheta0 β I.Λ R ≤ m → m ≤ M → ∀ (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ m)) (I.kappaSeq κ M m) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θm → IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev → I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) g θprev T → have S := √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x); have ε := epsilon β I.Λ (m - 1); have v := I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)); √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) s) x) ≤ A * S → √(spaceTimeGradNormSq (LeftToShow.materialGrad (streamVel (Φ (m - 1))) (T (Nstar β)))) ≤ A * ε ^ (3 * delta β) * (√(I.kappaSeq κ M (m - 1)))⁻¹ * S * (tauP β I.Λ m)⁻¹ → PositiveTemperatureJets A (ε ^ (1 + gamma β / 2)) S (T (Nstar β)) → Integration.InitialLayerContract I hΦ m (I.kappaSeq κ M m) θm T Ci S → (∀ t ∈ Set.Ioo 0 1, ∀ (x : Homogenization.Vec 2), sourceResidualIdentity I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T t x) → (∀ i < 10, ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => section5Term I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) (sourceErrorD I hΦ m (I.kappaSeq κ M m) (T (Nstar β))) (iterateError I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T) i p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)) → (∀ t ∈ Set.Ioo 0 1, Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) => twistie4 I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x + twistie5 I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x + normie3 I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x) → (∀ i < 10, timeHMinusOneNorm (Integration.section5CenteredTerm I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) (sourceErrorD I hΦ m (I.kappaSeq κ M m) (T (Nstar β))) (iterateError I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T) i) ≤ ENNReal.ofReal (Cr * √(I.kappaSeq κ M m) * ε ^ delta β * S)) → √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (v s) x - LeftToShow.leadingGrad I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s x) ≤ Ca * ε ^ (2 * delta β) * S → √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T (Nstar β) s) x - spaceGrad (θprev s) x) ≤ Ct * ε ^ (2 * delta β) * S → ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => LeftToShow.leadingGrad I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) p.1 p.2) (Set.Ici 0 ×ˢ Set.univ) → 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → |(I.kappaSeq κ M m * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θm s) x) - I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x| ≤ C * epsilon β I.Λ (m - 1) ^ delta β * (I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x)

Step-down conjunct (ii), conditional on the relative physical leaves. The witness precedes I; the temperature premises contain only positive jets and integrated gradients. The residual is assembled from all ten terms.