The vertical axis is Lebesgue-null

The vertical axis {x ∈ Vec3 | x₀ = x₁ = 0} — equivalently {polarR x = 0} — is a proper linear subspace of Vec3, hence Lebesgue-null by the general Haar-measure fact for strict subspaces. This is the "axis Lebesgue-null" step needed to integrate the off-axis pointwise vortex-stretching identity stretching_eq_stretchGTerm against a cutoff weight χ² over the whole ball (see lem:aniso:closure in the paper, arXiv:2609.20803).

theorem CIV.volume_axis_eq_zero : MeasureTheory.volume {x : CKN.Foundation.Parabolic.Vec3 | x 0 = 0 ∧ x 1 = 0} = 0

The vertical axis {x : Vec3 | x 0 = 0 ∧ x 1 = 0} has Lebesgue measure zero.

theorem CIV.volume_setOf_polarR_eq_zero_eq_zero : MeasureTheory.volume {x : CKN.Foundation.Parabolic.Vec3 | polarR x = 0} = 0

The set {x : Vec3 | polarR x = 0} has Lebesgue measure zero.

theorem CIV.ae_polarR_ne_zero : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), polarR x ≠ 0

Almost every point (with respect to Lebesgue measure) has polarR x ≠ 0.