hLeadingError from the S-amplitude temperature jets

Composition of the following steps:

• relative_iterate_gradient_jets (ATA): the θ_{m-1} profile and the V-increment amplitude conclusion, both with amplitude S, give the positive spatial jets of ∇T_i for every partial iterate;
• relative_Amnr_tensor_of_jets (ATB): the S-amplitude AMNR Hessian tensor estimate, from stream-function and diffusivity bounds and the actual recursion;
• relative_Hm_gradient_actual (ATC): on open time, √κ_m‖∇HTilde_m‖ ≤ CH ε^{4δ} S;
• relative_leading_error: the leading-error bound.

The remaining premises are hT0, hT1 and the two named upstream jets hTheta and hV, in their exact shapes with amplitude S.

theorem AVenhance.Infra.Section5.RelativeError.relative_leading_error_of_jets (β C₀ A Cs : ℝ) (hA : 1 ≤ A) (hCs : 0 < Cs) : ∃ (Ca : ℝ), 0 ≤ Ca ∧ ∃ (Λ₀ : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λ₀ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → have S := √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x); Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T A S → Integration.FirstOrderGradJetContract I m (I.kappaSeq κ M (m - 1)) T A S → ∀ (Rθ : ℝ), epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ → Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs S → Integration.VIncrementContract I m (I.kappaSeq κ M (m - 1)) T Cs Rθ S → √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s) x - LeftToShow.leadingGrad I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s x) ≤ Ca * epsilon β I.Λ (m - 1) ^ (2 * delta β) * S

RelativeLeaves.hLeadingError from the first-order T profile and the S-amplitude jets.