Actual finite-level source jets and their proved spatial base case.

structure AVenhance.Infra.Section4.AmnrSourceJetLevels {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (K : ℝ) (cut : ℕ) : Prop

Induction invariant for the actual velocity and its actual gradient. The velocity drift is excluded and each field pays its stream derivative cost.

• velocity (m : ℕ) (α : List (Fin 2)) (r : ℕ) : r ≤ cut → amnrMixedWord α r ≠ [] → α.length + 2 * r + 1 ≤ Nstar β → ∀ (i : Fin 2) (z : AmnrSpace), |amnrWord (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2) (amnrMixedWord α r) (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2 i) z| ≤ K * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ α.length * AVenhance.a β I.Λ m ^ r
• gradient (m : ℕ) (α : List (Fin 2)) (r : ℕ) : r ≤ cut → α.length + 2 * r + 2 ≤ Nstar β → ∀ (i p : Fin 2) (z : AmnrSpace), |amnrWord (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2) (amnrMixedWord α r) (amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2) i p) z| ≤ K * AVenhance.a β I.Λ m * (epsilon β I.Λ m)⁻¹ ^ α.length * AVenhance.a β I.Λ m ^ r

theorem AVenhance.Infra.Section4.amnrSourceJetLevels_spatial {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) : AmnrSourceJetLevels I Φ (max 1 (amnrSpatialVelocityConstant (Nstar β))) 0