orderParameterExamples
plain-language theorem explainer
orderParameterExamples enumerates five standard physical quantities that track the degree of ordering in phase transitions. A condensed-matter physicist would cite it when mapping J-cost minima to laboratory observables such as magnetization or density contrast. The definition is a direct list construction that pairs each system with its asymmetry measure.
Claim. The order-parameter examples are the list $((Ferromagnet, M), (Liquid-gas, ρ_l - ρ_g), (Superconductor, Δ), (Superfluid, condensate fraction), (Crystal, periodic density))$, where each pair records the measurable quantity that registers the asymmetry chosen by a J-cost minimum.
background
Module THERMO-006 derives phase transitions from bifurcations in the J-cost landscape. The J-cost is the recognition cost induced by a multiplicative recognizer on positive ratios; its local minima label stable phases, and an order parameter quantifies the asymmetry between those minima. The supplied doc-comment states that the J-cost itself remains symmetric while the selected minimum breaks symmetry.
proof idea
The definition is a direct list construction. It assembles the five canonical cases already listed in the doc-comment and links each to the J-cost asymmetry mechanism described in the module header.
why it matters
The list supplies concrete illustrations for the spontaneous-symmetry-breaking section that follows in the same module. It therefore supports the claim that phase transitions are J-cost bifurcations, the central proposition of the THERMO-006 paper draft. The examples also instantiate the T5 J-uniqueness step by exhibiting physical quantities that become nonzero once the fixed-point minimum is selected.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.