CriticalPoint

formal source

 123    Above critical point: No distinction between liquid and gas.
 124
 125    In RS: Critical point is where J-cost landscape changes topology. -/
 126structure CriticalPoint where
 127  temperature : ℝ
 128  pressure : ℝ
 129  is_singular : Bool
 130
 131/-- φ-connection to critical points?
 132
 133    Water: Tc/Tb = 647/373 ≈ 1.73 (close to √3 ≈ 1.73)
 134    Helium: Tc = 5.2 K, Tb = 4.2 K, Tc/Tb ≈ 1.24 (close to φ/1.3) -/
 135theorem critical_ratios :
 136    -- Tc/Tb may have φ-structure
 137    True := trivial
 138
 139/-! ## Order Parameter -/
 140
 141/-- The order parameter measures degree of ordering:
 142    - Magnetization for magnets
 143    - Density difference for liquid-gas
 144    - Superfluid fraction for He
 145
 146    In RS: Order parameter = asymmetry in J-cost minimum. -/
 147def orderParameterExamples : List (String × String) := [
 148  ("Ferromagnet", "Magnetization M"),
 149  ("Liquid-gas", "Density difference ρ_l - ρ_g"),
 150  ("Superconductor", "Gap Δ"),
 151  ("Superfluid", "Condensate fraction"),
 152  ("Crystal", "Periodic density")
 153]
 154
 155/-! ## Spontaneous Symmetry Breaking -/
 156