pith. machine review for the scientific record. sign in
theorem proved term proof

vortex_quantized

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  92theorem vortex_quantized (m : ℝ) (hm : 0 < m) :
  93    ∀ n : ℤ, n * vortex_quantum m = n * (2 * Real.pi / m) := fun _ => rfl

proof body

Term-mode proof.

  94
  95/-! ## Two-Fluid Model -/
  96
  97/-- RS critical exponent: α = ln φ / ln 2 ≈ 0.694.
  98    φ = (1+√5)/2 is the golden ratio. -/

depends on (6)

Lean names referenced from this declaration's body.