The relative terms field from the trace leaf and normie3 at S

The nine source producers at amplitude S = relS, all fed by the jet bundle SJets at one common (Cs, A) (a8Core); HmGradient at S from the θ profile; SourceErrorD from the jets; the mean-zero contracts from MeanZero.lean; R46 from the gradient contract (relativeTerms_contract_of_nine_sources_and_gradient). The only extra input is normie3 at S.

theorem AVenhance.Infra.Section5.Contracts.a8_nineSources_of_trace (β C₀ : ℝ) (hTr : A8TraceLeaf β C₀) (hN3 : ∃ (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))) : RelativeNineSourceProducers β C₀

The nine source producers at the relative amplitude, from the trace leaf and normie3.

theorem AVenhance.Infra.Section5.Contracts.a8_normie3S_of_trace (β C₀ : ℝ) (hTr : A8TraceLeaf β C₀) : ∃ (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) from the trace leaf: the producer normie3CenteredSource_contract fed by the S-amplitude jets, as for twistie5.

theorem AVenhance.Infra.Section5.Contracts.a8_terms_of_trace (β C₀ : ℝ) (hTr : A8TraceLeaf β C₀) (hN3 : ∃ (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))) : ∃ (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.RelativeTermsContract I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T C (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

The relative terms field from the trace leaf and normie3 at S.