Twistie5CenteredSourceContract

In the corrected form, twistie5 = -div(flux) (twistie5_eq_neg_div_flux) is a pure divergence of a smooth periodic flux, so the proof is flux-only: the centered HDot⁻¹ norm of a slice is at most the L² norm of the flux (sd_tw5_time_bound), which is pointwise ≲ ε_{m-1}^{2δ} ψ_m |∇T| (sd_flux_bound); integrating in time (sd_time_transfer) and using ψ_m² ≤ K κ_m κ_{m-1} together with TGradientContract gives the source right side C ε_{m-1}^δ √κ_m B. The jet hypotheses TPositiveJetsContract, FirstOrderGradJetContract of the earlier (ergodic) proof are no longer needed.

theorem AVenhance.Infra.Section5.Contracts.twistie5CenteredSource_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.Twistie5CenteredSourceContract I hΦ m (I.kappaSeq κ M m) T C B