Cutoff1SourceContract producer (e.monster.est.3, enhance.tex 7329–7364)

Conditional on TGradientContract β κ_{m-1} T A B (same amplitude B): on the support of ξ'_{m,k} the corrector is exponentially small (sb_corrTime_nonneg_le_decay), so that ‖cutoff1‖_{L²} ≲ e^{-c ε_{m-1}^{-2δ}} a_m ε_m ‖∇T‖_{L²}; the scale package turns this into C ε_{m-1}^δ √κ_m B.

theorem AVenhance.Infra.Section5.Contracts.sb_scalar_core {a εm E κm κp x K Cx M q δ : ℝ} (hK : 1 ≤ K) (hx : 0 < x) (hεm : 0 < εm) (hκm : 0 < κm) (h4 : a ^ 2 * εm ^ 4 / κm ≤ K * κp) (hq : x ^ q / 2 ≤ εm) (hE : E * (x ^ q)⁻¹ ≤ M * x ^ δ) (hE0 : 0 ≤ E) (hCx : 0 ≤ Cx) : Cx * (a * εm) * E ≤ Cx * (√K * √κm * √κp * (2 * (M * x ^ δ)))

Abstract-real core: the sharp constant of the pointwise bound is ≲ x^δ √(κ_m κ_{m-1}).

theorem AVenhance.Infra.Section5.Contracts.cutoff1Source_contract (β C₀ A : ℝ) (hA : 0 ≤ A) : ∃ (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 → Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T A B → Integration.Cutoff1SourceContract I hΦ m (I.kappaSeq κ M m) T C B

Cutoff1SourceContract producer (e.monster.est.3), at abstract amplitude B, from the T-gradient contract at the same amplitude.