Exact actual stream-matrix coefficient words and their continuity.

theorem AVenhance.Infra.Section4.iterateMatrixWord_stream {φ : Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateMatrixWord (fun (y : Homogenization.Vec 2) => φ y • sigmaMat) w x = iterateSpatialWord w φ x • sigmaMat

Every matrix word of the skew stream coefficient is the same scalar stream word times the fixed matrix.

theorem AVenhance.Infra.Section4.iterate_stream_matrix_word_continuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => φ z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (fun (y : Homogenization.Vec 2) => φ z.1 y • sigmaMat) w z.2) (Set.Ici 0 ×ˢ Set.univ)

All actual stream coefficient words are continuous jointly up to time zero, as required by the selected-flux space-time bound.