`TopologicalTransition`

definition

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.PhaseTransitions
domain: Thermodynamics
line: 226 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Thermodynamics.PhaseTransitions on GitHub at line 226.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 223    - Topological insulator transitions
 224
 225    In RS: Topology of J-cost landscape changes. -/
 226structure TopologicalTransition where
 227  winding_number_before : ℤ
 228  winding_number_after : ℤ
 229  is_continuous : Bool
 230
 231/-! ## Summary -/
 232
 233/-- RS picture of phase transitions:
 234
 235    1. **J-cost landscape**: Multi-dimensional surface
 236    2. **Minima**: Phases are local minima
 237    3. **First order**: Jump between separated minima
 238    4. **Second order**: Minima merge, fluctuations diverge
 239    5. **Critical point**: Topology change
 240    6. **Nucleation**: Thermal crossing of barriers -/
 241def summary : List String := [
 242  "Phases = J-cost minima",
 243  "First order = jump between minima",
 244  "Second order = merging minima",
 245  "Critical = topology change",
 246  "Nucleation = barrier crossing"
 247]
 248
 249/-! ## Falsification Criteria -/
 250
 251/-- The derivation would be falsified if:
 252    1. Phase transitions have no J-cost interpretation
 253    2. Critical behavior contradicts J-cost predictions
 254    3. Nucleation doesn't follow J-cost barriers -/
 255structure PhaseTransitionFalsifier where
 256  no_jcost_interpretation : Prop

papers checked against this theorem

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