def
definition
vortex_quantum
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.Superfluidity on GitHub at line 84.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
81/-! ## Quantized Vortices -/
82
83/-- Vortex circulation quantum κ = h/m (in natural units: 2π/m). -/
84noncomputable def vortex_quantum (m : ℝ) : ℝ := 2 * Real.pi / m
85
86/-- Vortex quantum is positive. -/
87theorem vortex_quantum_positive (m : ℝ) (hm : 0 < m) :
88 0 < vortex_quantum m := by
89 unfold vortex_quantum; positivity
90
91/-- Circulation is quantized: ∮ v_s dl = n × (2π/m). -/
92theorem vortex_quantized (m : ℝ) (hm : 0 < m) :
93 ∀ n : ℤ, n * vortex_quantum m = n * (2 * Real.pi / m) := fun _ => rfl
94
95/-! ## Two-Fluid Model -/
96
97/-- RS critical exponent: α = ln φ / ln 2 ≈ 0.694.
98 φ = (1+√5)/2 is the golden ratio. -/
99noncomputable def rs_critical_exponent : ℝ :=
100 Real.log ((1 + Real.sqrt 5) / 2) / Real.log 2
101
102/-- Golden ratio (1+√5)/2 > 1. -/
103private lemma golden_ratio_gt_one : 1 < (1 + Real.sqrt 5) / 2 := by
104 have h5 : 1 < Real.sqrt 5 := by
105 rw [show (1:ℝ) = Real.sqrt 1 from Real.sqrt_one.symm]
106 exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
107 linarith
108
109/-- Critical exponent is positive. -/
110theorem rs_critical_exponent_positive : 0 < rs_critical_exponent := by
111 unfold rs_critical_exponent
112 apply div_pos
113 · exact Real.log_pos golden_ratio_gt_one
114 · exact Real.log_pos (by norm_num)