`MetastableState`

definition

show as: view math explainer →

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

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

 179    - Supersaturated vapor
 180
 181    The system is stuck in a local J-cost minimum. -/
 182structure MetastableState where
 183  jcost_local_min : ℝ
 184  jcost_global_min : ℝ
 185  barrier_height : ℝ
 186  lifetime : ℝ  -- Time to nucleate
 187
 188/-- Nucleation: Crossing the J-cost barrier.
 189
 190    Thermal fluctuations can push system over barrier.
 191    Rate ~ exp(-ΔJ/kT) where ΔJ = barrier height. -/
 192noncomputable def nucleationRate (barrier : ℝ) (T : ℝ) (hT : T > 0) : ℝ :=
 193  exp (-barrier / (kB_SI * T))
 194
 195/-! ## Quantum Phase Transitions -/
 196
 197/-- Quantum phase transitions occur at T = 0:
 198
 199    Driven by quantum fluctuations, not thermal.
 200    Controlled by a non-thermal parameter (pressure, field, etc.).
 201
 202    In RS: These are pure J-cost transitions, no thermal noise. -/
 203structure QuantumPhaseTransition where
 204  control_parameter : ℝ
 205  critical_value : ℝ
 206  is_T_zero : Bool
 207
 208/-- Examples:
 209    - Mott insulator transition
 210    - Quantum Hall transitions
 211    - Heavy fermion criticality -/
 212def qptExamples : List String := [

papers checked against this theorem

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