pith. machine review for the scientific record. sign in
def definition def or abbrev

orderParameterExamples

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 147def orderParameterExamples : List (String × String) := [

proof body

Definition body.

 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 -/

depends on (20)

Lean names referenced from this declaration's body.