Initial-time L2 norm continuity from joint continuity on the closed half-line. This includes time zero, unlike an interior-time FTC interface.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_norm_continuous {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (b : ℝ) : ContinuousOn (fun (t : ℝ) => √(l2NormSq (F t))) (Set.Icc 0 b)

A jointly continuous cell field has continuous L2 norm, including its initial slice. There is no size or normalization hypothesis.