QuantumPhaseTransition
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not compute the critical value from any microscopic Hamiltonian.
- Does not classify the transition as first-order or second-order.
- Does not incorporate finite-temperature corrections.
- Does not enforce any functional relation between the control parameter and the critical value.
formal statement (Lean)
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 -/