Joint datum jets with one uniform coefficient

theorem AVenhance.Infra.Section5.Contracts.tJets_datum_contract (β Ccut : ℝ) : ∃ (A : ℝ) (C₁ : ℝ), 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 → ℝ) => have B := √(l2NormSq θ₀); Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T A B ∧ Integration.TPositiveJetsContract I m 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

All jets needed by the source producers, with the same datum amplitude and coefficient. The coefficient and threshold precede the ingredients.