Twistie1HMinusSourceContract producer (e.monster.est.5, enhance.tex 7371–7460)

twistie1HMinusSource_contract produces Twistie1HMinusSourceContract at an abstract amplitude B conditionally on the contracts TPositiveJetsContract (slice jets of T), TGradientContract, FirstOrderGradJetContract, SecondOrderGradJetContract (space-time L² of ∇ ∂^w T, |w| ≤ 2, at the same amplitude B) and Twistie1MeanZeroContract (total mean zero).

The proof follows the source: the ergodic lemma with the choice e.fg.choice.1 gives, for each (k, j), a main term ε_m ‖f‖_{L²} ‖g‖_{L²} and an exponentially small term (centered_frozen_hMinusOneNorm_le_of_fastPeriodicProduct_flow); the main term is ε_m · ε_m^{1-γ} · ‖∇ ∇·((K_m + s_{m-1}) ∇T)‖_{L²} with ‖∇ ∇·((K_m + s_{m-1}) ∇T)‖ ≲ √κ_{m-1} ε_{m-1}^{-(2+γ)} B, and the scale exponent is 8δ ≥ δ (se_main_scale).

theorem AVenhance.Infra.Section5.Contracts.twistie1HMinusSource_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.TPositiveJetsContract I m T A B → Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T A B → Integration.FirstOrderGradJetContract I m (I.kappaSeq κ M (m - 1)) T A B → Integration.SecondOrderGradJetContract I m (I.kappaSeq κ M (m - 1)) T A B → Integration.Twistie1MeanZeroContract I hΦ m (I.kappaSeq κ M m) T → Integration.Twistie1HMinusSourceContract I hΦ m (I.kappaSeq κ M m) T C B

Twistie1HMinusSourceContract producer (e.monster.est.5), at abstract amplitude B.