QuantumPhaseTransition
plain-language theorem explainer
QuantumPhaseTransition packages the data for a zero-temperature transition driven by quantum fluctuations alone in the J-cost landscape. Condensed-matter physicists working on Mott insulators or quantum Hall systems would cite the structure when mapping a laboratory tuning parameter to its Recognition Science critical value. The declaration is a bare structure definition with three fields and no attached computation or lemmas.
Claim. A quantum phase transition is given by a real control parameter $λ$, a real critical value $λ_c$, and a boolean flag indicating that the transition occurs at zero temperature.
background
The module derives phase transitions from bifurcations in the J-cost landscape, where the J-cost function is the Recognition Science cost J(x) = (x + x^{-1})/2 - 1. Multiple local minima of this landscape merge or split as a control parameter varies, producing first-order, second-order, or critical-point behavior. Quantum phase transitions are the special case with no thermal noise, so the transition is controlled solely by a non-thermal parameter such as pressure or magnetic field.
proof idea
The declaration is a structure definition that simply records three fields. No lemmas are invoked and no tactics are used.
why it matters
The structure supplies the data type needed to record quantum phase transitions inside the thermodynamics module, directly supporting the claim that all phase transitions arise as J-cost bifurcations. It isolates the T = 0 limit consistent with the J-uniqueness property and the eight-tick octave of the forcing chain. The module documentation links the construction to the paper proposition on phase transitions as information-theoretic bifurcations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.