vortex_quantum_positive
plain-language theorem explainer
Positivity of the vortex circulation quantum holds for any positive real mass parameter. Researchers modeling superfluid helium in the Recognition Science setting cite it to fix the sign of κ in natural units. The argument is a one-line term proof that unfolds the definition and applies positivity.
Claim. If $m > 0$, then $2π/m > 0$.
background
The module derives superfluidity from RS eight-tick coherence, treating He-4 as a BEC of integer-spin bosons and He-3 via Cooper pairing of fermions. Quantized vortices arise from U(1) gauge invariance, with circulation quantum defined explicitly as 2 * Real.pi / m in units where ħ = 1. Upstream results supply collision-free empirical programs, simplicial edge lengths from psi, and mechanism-design structures that ground the ledger before the positivity step.
proof idea
The term proof unfolds the definition of vortex_quantum to expose 2 * Real.pi / m, then invokes the positivity tactic to discharge the strict inequality under the hypothesis m > 0.
why it matters
The result secures the sign of the circulation quantum inside the superfluidity model built on eight-tick coherence. It directly supports the module claim that quantized vortices follow from U(1) gauge invariance in RS_Superfluidity.tex. No downstream theorems are recorded, so the declaration functions as a basic sign check rather than a bridge to further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.