`vortex_quantized`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.Superfluidity
domain: Physics
line: 92 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.Superfluidity on GitHub at line 92.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  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)
 115
 116/-- Superfluid fraction: ρ_s(T)/ρ = 1 - (T/Tlam)^α. -/
 117noncomputable def superfluid_fraction (T Tlam : ℝ) : ℝ :=
 118  1 - (T / Tlam) ^ rs_critical_exponent
 119
 120/-- At T = 0, fully superfluid. -/
 121theorem superfluid_fraction_at_zero (Tlam : ℝ) (hTlam : 0 < Tlam) :
 122    superfluid_fraction 0 Tlam = 1 := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.