Axisymmetry on the unit cylinder from analytic forcing and an axisymmetric core

The first half of the proof of thm:main: by interior analyticity thm:analytic:interior, spatial analyticity of the force eq:interior:force:analytic makes every slice u(·, t) real analytic on B(1), and the identity theorem carries the exact axisymmetry on the core eq:interior:core to all of Q, which is eq:interior:global:symmetry.

theorem CIV.isAxisymmetricOn_unitCylinder_of_forceSpatiallyAnalytic {q : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hfa : ForceSpatiallyAnalytic f) (hcore : ∀ t ∈ Set.Ioo (-1) 0, ∃ ρ ∈ Set.Ioo 0 1, IsAxisymmetricOn u (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) {t})) : IsAxisymmetricOn u unitCylinder

eq:interior:global:symmetry: a suitable weak solution on Q, smooth there, with a spatially analytic force and an axisymmetric core at every time, is axisymmetric on Q.