SourceErrorDContract producers

sourceErrorD_of_jets_contract produces SourceErrorDContract at an abstract amplitude B, conditionally on the three existing contracts at that amplitude: ThetaProfileContract, VIncrementContract, TGradientContract. sourceErrorD_contract is the exact unconditional producer at the big-bound/step-down part (i) amplitude B = ‖θ₀‖.

Route (paper p.dm.bounds with N_* large):

• the first summand Σ_l ξ̂_{m,l} F_lᵀ (JHat_m - J_m) F_l ∇T is bounded in L² by 2 F_gap · 4 L² ‖∇T‖ with L = 2 (stream-function flow Jacobian bound on active windows, dm_flowGrad_norm_le_two_of_A3; ‖∇T‖_{L²} by the T profile through the time clamp, sed_Tgrad_eLpNorm_le), where F_gap is the flux gap bound (flux_sub_Jhat_norm_le);
• the tail Σ_n A_{m,n,Jcut} q_{m,n,Jcut} uses the terminal AMNR tensor (sed_tail_amnr_of_jets, from the ∇T_i jets of relative_iterate_gradient_jets) and the geometric qMNR bound;
• both are of the paper scale √κ_{m-1} (C ε_{m-1}^{δ/2})^{Jcut}, which is at most C ε_{m-1}^{2δ} √κ_m because δ Jcut / 2 ≥ 2δ + qβ and ε_m^{2β} ≤ K κ_{m-1} κ_m (sed_final_scale).

theorem AVenhance.Infra.Section5.Contracts.sed_K2_rpow {β : ℝ} (I : Ingredients β) (m : ℕ) {κm κp K : ℝ} (hκm : 0 < κm) (h : a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κm ≤ K * κp) : epsilon β I.Λ m ^ (2 * β) ≤ K * κp * κm

a_m² ε_m⁴ = ε_m^{2β}, hence a_m² ε_m⁴/κ_m ≤ K κ_{m-1} gives ε_m^{2β} ≤ K κ_{m-1} κ_m.

theorem AVenhance.Infra.Section5.Contracts.sourceErrorD_of_jets_contract (β C₀ Cs A : ℝ) (hCs : 0 < Cs) (hA : 0 ≤ A) : ∃ (Cd : ℝ) (C₁ : ℝ), 0 ≤ Cd ∧ Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (_θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => ∀ (B : ℝ), 0 ≤ B → ∀ (Rθ : ℝ), epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ → Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs B → Integration.VIncrementContract I m (I.kappaSeq κ M (m - 1)) T Cs Rθ B → Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T A B → Integration.SourceErrorDContract I hΦ m (I.kappaSeq κ M m) T Cd B

SourceErrorDContract producer, abstract amplitude B, conditional on the θ profile, the V increments and the integrated T gradient at that amplitude.

theorem AVenhance.Infra.Section5.Contracts.sourceErrorD_contract (β C₀ : ℝ) : ∃ (Cd : ℝ) (C₁ : ℝ), Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Integration.SourceErrorDContract I hΦ m (I.kappaSeq κ M m) T Cd √(l2NormSq θ₀)

SourceErrorDContract producer, exact unconditional form at the big-bound/step-down part (i) amplitude B = ‖θ₀‖_{L²} (e.monster.est.11.a.d). Constants (Cd, the Λ-threshold) depend only on β, C₀.