The integrated second-order T jet (e.nabm2, n = 2)

The two-letter word estimate includes the gradient energy. Its factorial is absorbed in a coefficient chosen before the ingredients; the amplitude stays abstract in the conditional producer.

theorem AVenhance.Infra.Section5.Contracts.secondOrderGradJet_bound_of_constants {P D A B r x : ℝ} (hP : 0 ≤ P) (hD : 0 ≤ D) (hB : 0 ≤ B) (hr : 0 < r) (hPA : 2 * P ≤ A) (hDA : D ≤ A) (hx : x ≤ B * P * 2 * (D / r) ^ 2) : x ≤ A * (A / r) ^ 2 * B

theorem AVenhance.Infra.Section5.Contracts.secondOrderGradJet_of_thetaProfile_contract (β Ccut CsReq : ℝ) : ∃ (Cs : ℝ) (A : ℝ) (C₁ : ℝ), CsReq ≤ Cs ∧ 1 ≤ Cs ∧ 1 ≤ A ∧ Integration.OnA7Instances β Ccut 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.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs B → Integration.SecondOrderGradJetContract I m (I.kappaSeq κ M (m - 1)) T A B

Exact abstract-amplitude second-order contract from the theta profile, with its coefficient above the requested lower bound.