Polar REq Zero

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.polarR_eq_zero_iff (x : CKN.Foundation.Parabolic.Vec3) : polarR x = 0 ↔ x 0 = 0 ∧ x 1 = 0

polarR x = 0 exactly when the point lies on the vertical axis: x 0 = 0 and x 1 = 0.