TinyHMinusSourceContract producer (e.monster.est.tiny, enhance.tex 7848–7930)

tinyHMinusSource_contract produces TinyHMinusSourceContract at an abstract amplitude B, conditionally on three contracts at the same amplitude: SourceErrorDContract (d_m), VIncrementContract (the increments of the T-iterates, hence e_{m-1} and ∇∇·e_{m-1}) and TinyMeanZeroContract (mean of tinyNondivergencePart).

The proof follows the source: hMinusOneNorm_tiny_le_of_components splits tiny into the divergence part (bounded by ‖d + e‖_{L²}) and the nondivergence part (bounded in L² by sup|χTilde| · ‖∇∇·e‖_{L²}); e = -B ∇V is expanded by the ordered Leibniz rule with the coefficient jets of B = K_m - κ_{m-1} + s_{m-1}; the factor x^{δ N*} of the last increment beats every negative power of ε_{m-1} (sc_delta_Nstar_budget).

theorem AVenhance.Infra.Section5.Contracts.sc_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.tinyHMinusSource_contract (β C₀ Cd Cs : ℝ) (hCd : 0 ≤ Cd) (hCs : 0 ≤ Cs) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (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 → ℝ) => ∀ (B : ℝ), 0 ≤ B → ∀ (Rθ : ℝ), epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ → Integration.SourceErrorDContract I hΦ m (I.kappaSeq κ M m) T Cd B → Integration.VIncrementContract I m (I.kappaSeq κ M (m - 1)) T Cs Rθ B → Integration.TinyMeanZeroContract I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T → Integration.TinyHMinusSourceContract I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T C B

TinyHMinusSourceContract producer (e.monster.est.tiny), at abstract amplitude B.