Step-down and main theorem from the five leaves

A8Leaves β C₀ collects the five leaves that remain after the seven relative fields of A8Remaining are derived from the S-amplitude trace (thetaProfile_S_contract_of_T1h, the T/V/HTilde jet producers, the nine abstract-amplitude source producers, relative_leading_error_of_jets, temperatureError_of_thetaProfile_contract, initialLayer_from_relative_profiles).

structure AVenhance.Infra.Section5.Contracts.A8Leaves (β C₀ : ℝ) : Prop

The five leaves of step-down.

• normie3 : ∃ (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.Normie3CenteredSourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

  normie3 at the datum amplitude.

• normie3S : ∃ (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 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → Integration.Normie3CenteredSourceContract I hΦ m (I.kappaSeq κ M m) T C (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

  normie3 at the relative amplitude S, gate.

• 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

  HTilde sup at the datum amplitude.

• iterate : ∃ (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.SectionFourIterateContract I m θ₀ θprev T C

  e.Tm.thetam at the datum amplitude.

• t1hTrace : ∃ (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 S-amplitude positive initial trace, gate.

theorem AVenhance.Infra.Section5.Contracts.a8Remaining_of_leaves (β C₀ : ℝ) (h : A8Leaves β C₀) : A8Remaining β C₀

Step-down inputs from the five leaves: all ten fields of A8Remaining.

theorem AVenhance.Infra.Section5.Contracts.indystepdown_of_leaves (β C₀ : ℝ) (h : A8Leaves β C₀) : Integration.IndyStepDownStatement β C₀

Step-down from the five leaves: the literal step-down statement (both conjuncts).

structure AVenhance.Infra.Section5.Contracts.A8LeavesLeftJacobian (β C₀ : ℝ) : Prop

The three step-down leaves left after: both normie3 leaves are produced (normie3CenteredSource_datum_closed_contract, a8_normie3S_of_trace).

• 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

  HTilde sup at the datum amplitude.

• iterate : ∃ (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.SectionFourIterateContract I m θ₀ θprev T C

  e.Tm.thetam at the datum amplitude.

• t1hTrace : ∃ (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 S-amplitude positive initial trace, gate.

theorem AVenhance.Infra.Section5.Contracts.a8Leaves_of_e53 (β C₀ : ℝ) (h : A8LeavesLeftJacobian β C₀) : A8Leaves β C₀

theorem AVenhance.Infra.Section5.Contracts.indystepdown_of_leaves_e53 (β C₀ : ℝ) (h : A8LeavesLeftJacobian β C₀) : Integration.IndyStepDownStatement β C₀

Step-down from the three leaves.