Ordered spatial derivatives remain smooth up to the initial time. At the boundary the proof uses the within derivative, not an unsupported ambient derivative of the extension to negative times.

theorem AVenhance.Infra.Section4.iterate_spatial_partial_smooth_up_to_initial {f : AmnrSpace → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => spaceGrad (fun (y : Homogenization.Vec 2) => f (z.1, y)) z.2 i) (Set.Ici 0 ×ˢ Set.univ)

Differentiate only in space on the closed nonnegative-time domain.

theorem AVenhance.Infra.Section4.iterateSpatialWord_smooth_up_to_initial {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => iterateSpatialWord w (u z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)

All ordered spatial derivatives of the actual scalar retain joint smoothness on the closed time domain, including their initial trace.

theorem AVenhance.Infra.Section4.iterate_classical_word_initial {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F u₀ u) (w : List (Fin 2)) : iterateSpatialWord w (u 0) = iterateSpatialWord w u₀

The initial trace of a spatial word is the corresponding initial-data word. This uses a function equality, without ambient derivatives at time zero.