Step-down producer helper

Step-down (IndyStepDownStatement) from the three leaves, two of which are produced here: iterate and the S-amplitude trace. The only remaining hypothesis is the HTilde sup leaf HmSupContract at the datum amplitude.

theorem AVenhance.Infra.Section5.Contracts.t1hTrace_leaf_contract (β C₀ : ℝ) : ∃ (Ctr : ℝ), 1 ≤ Ctr ∧ ∃ (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 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → T1hThetaInitialTraceInput β I κ M m θ₀ θprev Ctr

The produced S-amplitude trace leaf, in the A8LeavesLeftJacobian shape.

theorem AVenhance.Infra.Section5.Contracts.indystepdown_of_hmSup (β C₀ : ℝ) (hmSup : ∃ (C : ℝ) (C₁ : ℝ), Integration.OnA7Instances β C₀ 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.HmSupContract I hΦ m (I.kappaSeq κ M m) θ₀ T C) : Integration.IndyStepDownStatement β C₀

Step-down from the HTilde sup leaf alone (every other leaf produced).

theorem AVenhance.Infra.Section5.Contracts.hmSup_leaf_of_piolaRate (β C₀ : ℝ) (hP : ∃ (Creg : ℝ) (C₁ : ℝ), Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => HmPiolaSourceRate I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T Creg √(l2NormSq θ₀)) : ∃ (C : ℝ) (C₁ : ℝ), Integration.OnA7Instances β C₀ 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.HmSupContract I hΦ m (I.kappaSeq κ M m) θ₀ T C

The HTilde sup leaf from the Piola-source rate family.

theorem AVenhance.Infra.Section5.Contracts.indystepdown_of_piolaRate (β C₀ : ℝ) (hP : ∃ (Creg : ℝ) (C₁ : ℝ), Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => HmPiolaSourceRate I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T Creg √(l2NormSq θ₀)) : Integration.IndyStepDownStatement β C₀

Step-down from the Piola-source rate alone (every other leaf produced).