pith. machine review for the scientific record. sign in
structure

SecondOrderTransition

definition
show as:
view math explainer →
module
IndisputableMonolith.Thermodynamics.PhaseTransitions
domain
Thermodynamics
line
105 · github
papers citing
none yet

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

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

open explainer

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 :