vortex_quantized
plain-language theorem explainer
The declaration establishes that vortex circulation in the RS superfluid model equals an integer multiple of the quantum 2π/m. Physicists deriving quantized vortex lines in superfluid helium from eight-tick coherence would cite it to link U(1) gauge invariance to observable circulation. The proof is a one-line reflexivity that follows directly from the definition of the vortex quantum.
Claim. Let $m > 0$ be a mass parameter. For every integer $n$, the circulation satisfies $n · κ = n · (2π/m)$, where $κ := 2π/m$ denotes the vortex quantum.
background
The module treats superfluid He-4 as a Bose-Einstein condensate of integer-spin (8-tick) bosons and superfluid He-3 as Cooper-paired fermions, with quantized vortices arising from U(1) gauge invariance. The vortex quantum is introduced as the noncomputable definition κ(m) = 2π/m in natural units. Upstream dependencies include the Model structure from LawOfExistence (ensuring positive constants) and the vortex_quantum definition itself.
proof idea
The proof is a one-line term that applies reflexivity to the definition of vortex_quantum, confirming equality after scaling by any integer n.
why it matters
This places quantized vortices inside the RS eight-tick coherence framework, directly supporting the two-fluid model for superfluid helium as described in the module documentation. It fills the circulation quantization step that follows from gauge invariance and connects to the forcing chain's T7 octave. No downstream theorems are listed yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.