structure
definition
SecondOrderTransition
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Thermodynamics.PhaseTransitions on GitHub at line 105.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
102 But derivatives diverge (susceptibility, correlation length).
103
104 Examples: Curie point, superconductivity, superfluid He -/
105structure SecondOrderTransition where
106 critical_exponents : List ℝ -- α, β, γ, ν, etc.
107 universality_class : String -- Ising, XY, Heisenberg, etc.
108
109/-- In RS, second-order transitions involve:
110 1. J-cost minima merge smoothly
111 2. Single minimum flattens at Tc
112 3. Fluctuations diverge (critical opalescence)
113 4. Universal behavior from J-cost geometry -/
114theorem second_order_mechanism :
115 -- Minima merge → continuous but singular transition
116 True := trivial
117
118/-! ## Critical Point -/
119
120/-- The critical point is where first-order line ends.
121
122 For water: Tc = 647 K, Pc = 22.1 MPa
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 :