Conditional assembly of the step-down estimate initial-layer contract from the Hm bound

theorem AVenhance.Infra.Section5.Contracts.initialLayer_from_HmSup (β C₀ CHs : ℝ) : ∃ (Cᵢ : ℝ) (C₁ : ℝ), Integration.OnA8Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm _θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Integration.HmSupContract I hΦ m (I.kappaSeq κ M m) θ₀ T CHs → Integration.InitialLayerContract I hΦ m (I.kappaSeq κ M m) θm T Cᵢ √(l2NormSq θ₀)

Assemble the exact step-down estimate initial-layer contract from the matching positive-time HmSupContract. The sole additional premise is exposed as a conditional helper; the exact family producer still requires a proof that the Hm bound follows from the step-down estimate data.