The S-amplitude core of step-down and six relative fields from the trace leaf

From the single leaf t1hTrace (the S-amplitude positive initial trace under the gate) we derive the θ profile at every large enough radius constant (thetaProfile_S_contract_of_T1h) and a bundle SJets of the T and V contracts at one common coefficient pair (Cs, A); the six relative fields gradient, material, jets, relative_initial, leading, temperature then follow.

structure AVenhance.Infra.Section5.Contracts.SJets {β : ℝ} (I : Ingredients β) (m : ℕ) (κprev : ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (R Cs A S : ℝ) : Prop

The S-amplitude temperature jets of one block instance, at one common (Cs, A).

• profile : Integration.ThetaProfileContract I m κprev θprev Cs S
• grad : Integration.TGradientContract β κprev T A S
• pos : Integration.TPositiveJetsContract I m T A S
• first : Integration.FirstOrderGradJetContract I m κprev T A S
• second : Integration.SecondOrderGradJetContract I m κprev T A S
• vinc : Integration.VIncrementContract I m κprev T Cs R S

@[reducible, inline]

abbrev AVenhance.Infra.Section5.Contracts.SJetsP (β Cs A : ℝ) : A8Pred β

SJets as a block predicate, at the relative amplitude.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.Contracts.a8Core (β C₀ : ℝ) (hTr : ∃ (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) : ∃ (CsS : ℝ), 1 ≤ CsS ∧ (∀ (Cs : ℝ), CsS ≤ Cs → ∃ (L : ℝ), Integration.OnA8Instances β C₀ L 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.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs (relS I κ M m θprev)) ∧ ∃ (Cs : ℝ) (A : ℝ) (L : ℝ), CsS ≤ Cs ∧ 1 ≤ Cs ∧ 1 ≤ A ∧ Integration.OnA8Instances β C₀ L 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 → SJets I m (I.kappaSeq κ M (m - 1)) θprev T R Cs A (relS I κ M m θprev)

The S-amplitude core: the θ profile at every radius constant above CsS, and the jet bundle at a common (Cs, A), all under the gate and all derived from the trace leaf.