Uniform assembly of the exact relative initial-layer contract from the genuine gradient trace and iterate spatial jets. No Hm estimate is assumed.

theorem AVenhance.Infra.Section5.Contracts.initialLayer_from_relative_jets (β C₀ Ctrace Cg Cl : ℝ) (hCg : 0 ≤ Cg) (hCl : 1 ≤ Cl) : ∃ (Ci : ℝ) (C₁ : ℝ), Integration.OnA8Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (g : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => have ν := I.kappaSeq κ M (m - 1); have S := √ν * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev t) x); (∀ (i : Fin 2), √(l2NormSq fun (x : Homogenization.Vec 2) => spaceGrad g x i) ≤ Ctrace * ↑(Nat.factorial 1) * (Ctrace / epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) ^ 1 * S) → (∀ i ≤ Nstar β, ∀ (p : Fin 2) (α : List (Fin 2)), α.length ≤ Nstar β → MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (_Φ (m - 1)) y.1 y.2) (List.map some α) (Section4.amnrTGradient (T i) p)) 2 ((MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod (MeasureTheory.volume.restrict unitCube)) ≤ ENNReal.ofReal (Cg * S / √ν * (Cl * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ α.length)) → Integration.InitialLayerContract I hΦ m (I.kappaSeq κ M m) θm T Ci S

Constants precede the step-down estimate data. The only remaining inputs are the initial n=1 gradient trace and the gradient-only spatial jets of the actual iterates.