Natural regularity and periodicity of the explicit velocity terms.

theorem AVenhance.Infra.Section4.iterateVelocitySplit_periodic {b : Homogenization.Vec 2 → Homogenization.Vec 2} {v : Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hv : ContDiff ℝ (↑⊤) v) (hbp : IsZ2Periodic b) (hvp : IsZ2Periodic v) (P : List (List (Fin 2) × List (Fin 2))) : IsZ2Periodic (iterateVelocitySplit P b v)

Velocity and scalar periodicity pass to every differentiated split term.

theorem AVenhance.Infra.Section4.iterateVelocitySplit_continuousOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {v : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (P : List (List (Fin 2) × List (Fin 2))) : ContinuousOn (fun (z : AmnrSpace) => iterateVelocitySplit P (b z.1) (v z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)

Joint continuity of the split sum follows from the actual smooth carriers up to zero, independently of the material error's ambient derivative at zero.