`orderParameterExamples`

definition

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.PhaseTransitions
domain: Thermodynamics
line: 147 · 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 147.

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

 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
 157/-- Symmetry breaking: High-T symmetric, low-T asymmetric.
 158
 159    The J-cost is symmetric in order parameter.
 160    But the minimum chosen breaks symmetry.
 161
 162    Examples:
 163    - Magnet: Up/down symmetry → all spins align (one direction)
 164    - Crystal: Translation symmetry → periodic structure -/
 165theorem spontaneous_symmetry_breaking :
 166    -- Symmetric J-cost → asymmetric ground state
 167    True := trivial
 168
 169/-- In RS, SSB is J-cost selecting one of equivalent minima.
 170    Random choice, but then frozen in. -/
 171def ssbMechanism : String :=
 172  "System falls into one of equivalent J-cost minima"
 173
 174/-! ## Nucleation and Metastability -/
 175
 176/-- For first-order transitions, metastable states exist:
 177    - Supercooled liquid

papers checked against this theorem

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