Normie3CenteredSourceContract

In the corrected form, normie3 = Σ_k ξ_k frob (F_kᵀ (𝒥 - C⁰_k)) ∇G_k with C⁰_k = cellFluxCell ∘ Y_k, whose fast factor 𝒥 - cellFluxCell has exact zero cell mean on supp ξ_{m,k}. There is no divergence part: the whole of normie3 is a locally finite sum of fast-slow products, and the centered ergodic estimate of Contracts/TermCenteredNd.lean bounds its HDot⁻¹ norm at a fixed time. Time integration (sd_time_transfer) and the scale arithmetic (n3_arith_final, n3_scale1, n3_exp_scale; exponent identity q(1 - γ) - 1 - γ/2 = 4δ) give C ε_{m-1}^δ √κ_m B. Inputs at amplitude B: TPositiveJetsContract, TGradientContract, FirstOrderGradJetContract.

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