Closing datum source producers with the proved T jets

theorem AVenhance.Infra.Section5.Contracts.cutoff1Source_datum_closed_contract (β Ccut : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), 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 → ℝ) => Integration.Cutoff1SourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

Exact datum producer, with every jet input discharged.

theorem AVenhance.Infra.Section5.Contracts.twistie3Source_datum_closed_contract (β Ccut : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), 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 → ℝ) => Integration.Twistie3SourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

Exact datum producer, with every jet input discharged.

theorem AVenhance.Infra.Section5.Contracts.normie1Source_datum_closed_contract (β Ccut : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), 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 → ℝ) => Integration.Normie1SourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

Exact datum producer, with every jet input discharged.

theorem AVenhance.Infra.Section5.Contracts.twistie4CenteredSource_datum_closed_contract (β Ccut : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), 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 → ℝ) => Integration.Twistie4CenteredSourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

Exact datum producer, with every jet input discharged.

theorem AVenhance.Infra.Section5.Contracts.twistie5CenteredSource_datum_closed_contract (β Ccut : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), 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 → ℝ) => Integration.Twistie5CenteredSourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

Exact datum producer, with every jet input discharged.

theorem AVenhance.Infra.Section5.Contracts.twistie1HMinusSource_datum_closed_contract (β Ccut : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), 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 → ℝ) => Integration.Twistie1HMinusSourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

Exact datum producer, with every jet input discharged.

theorem AVenhance.Infra.Section5.Contracts.normie3CenteredSource_datum_closed_contract (β Ccut : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), 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 → ℝ) => Integration.Normie3CenteredSourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

Exact datum producer of the normie3 centered contract, with every jet input discharged.