Uniform minimal material estimate from the abstract-amplitude theta profile.

theorem AVenhance.Infra.Section5.Contracts.tMaterial_of_thetaProfile_contract (β Ccut CsReq : ℝ) (hReq : 1 ≤ CsReq) : ∃ (Cs : ℝ) (A : ℝ) (C₁ : ℝ), CsReq ≤ Cs ∧ 0 ≤ 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 → ℝ) => ∀ (S : ℝ), 0 ≤ S → Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs S → Integration.TMaterialContract I Φ m (I.kappaSeq κ M (m - 1)) T A S

All source inputs of the first material step are discharged. The only remaining temperature input is the independently owned theta profile. The radius may be enlarged before the instance is selected.