Exact finite-order spatial slice bridges for the actual flux.

theorem AVenhance.Infra.Section4.amnrWord_spatial_slice_on_vertical_domain_finite {U : Set AmnrSpace} (hU : IsOpen U) {f : AmnrSpace → ℝ} {N : ℕ} (hf : ContDiffOn ℝ (↑N) f U) (b : AmnrSpace → Homogenization.Vec 2) (α : List (Fin 2)) (hα : α.length ≤ N) (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

Spatial words require only their own ordinary derivative count; they do not infer infinite joint regularity from the finite source coefficient.