Spatial-word bridges on the actual open cutoff neighborhood.

theorem AVenhance.Infra.Section4.amnrWord_spatial_slice_on_vertical_domain {U : Set AmnrSpace} (hU : IsOpen U) {f : AmnrSpace → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (b : AmnrSpace → Homogenization.Vec 2) (α : List (Fin 2)) (t : ℝ) (hvertical : ∀ (x : Homogenization.Vec 2), (t, x) ∈ U) (x : Homogenization.Vec 2) : amnrWord b (List.map some α) f (t, x) = amnrSpaceWord α (fun (y : Homogenization.Vec 2) => f (t, y)) x

An open joint smoothness domain containing the whole time slice is sufficient to identify actual ordered spatial words with slice derivatives.

noncomputable def AVenhance.Infra.Section4.amnrFlowGradientSpatialConstant (N : ℕ) : ℝ

One constant controls the entire finite spatial budget of the actual pulled Jacobian's ordered words.

Equations

• AVenhance.Infra.Section4.amnrFlowGradientSpatialConstant N = ↑N.factorial * AVenhance.Infra.Section4.amnrFlowSpatialSourceConstant N ^ (N + 1)

theorem AVenhance.Infra.Section4.amnrFlowGradientSpatialConstant_pos (N : ℕ) : 0 < amnrFlowGradientSpatialConstant N

theorem AVenhance.Infra.Section4.amnr_flowGrad_spatialWord_abs_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (z : AmnrSpace) (ht : |z.1 - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) (α : List (Fin 2)) (hbudget : α.length ≤ Nstar β) (i j : Fin 2) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (fun (y : AmnrSpace) => I.flowGrad hΦ m l y.1 y.2 i j) z| ≤ amnrFlowGradientSpatialConstant (Nstar β) * (epsilon β I.Λ (m - 1))⁻¹ ^ α.length

The actual spatial part of the source flow primitive now has its full paper budget and a scale-independent constant.