twoLevelSystem
A definition that builds a two-level system with ground-state energy 0 and excited-state energy equal to the input gap parameter, each carrying degeneracy 1. Workers deriving the Boltzmann distribution from J-cost in Recognition Science cite this when specializing the general System type to the qubit case. The construction enumerates two EnergyLevel records inside the System structure and discharges the nonempty obligation by norm_num.
claimLet $Δ ∈ ℝ$. The two-level system is the structure whose energy levels consist of the ground state at energy 0 with degeneracy 1 together with the excited state at energy $Δ$ with degeneracy 1.
background
The module derives the Boltzmann distribution from Recognition Science's J-cost functional, where lower-cost states are more probable under a fixed total-cost constraint. A System is a non-empty list of EnergyLevel records; each EnergyLevel pairs a real energy with a positive integer degeneracy. Upstream, the probability definition from QuantumLedger supplies the Born-rule interpretation later used to normalize Boltzmann weights, while the gap definitions from Gap45 and the mass anchors supply the numerical scale that will be inserted for concrete calculations.
proof idea
The definition directly populates the levels field of the System structure with two EnergyLevel constructors (ground state at 0, excited state at the supplied gap, each of degeneracy 1) and discharges the nonempty field by a norm_num tactic confirming positive list length.
why it matters in Recognition Science
This supplies the minimal concrete instance required to illustrate cost-weighted state selection inside the THERMO-001 derivation of statistical mechanics from the J-cost functional and Recognition Composition Law. It precedes the partitionFunction and probability siblings that produce the explicit Boltzmann factor exp(-βE)/Z. No open questions or scaffolding remain; the definition is a finished building block for the paper proposition on RS-native thermodynamics.
scope and limits
- Does not introduce inverse temperature or the partition function.
- Does not require the gap parameter to be positive.
- Does not link the gap to the phi-ladder or mass formulas.
- Does not compute or normalize probabilities; those steps occur in sibling definitions.
formal statement (Lean)
253def twoLevelSystem (gap : ℝ) : System := {
proof body
Definition body.
254 levels := [
255 ⟨0, 1, by norm_num⟩, -- Ground state
256 ⟨gap, 1, by norm_num⟩ -- Excited state
257 ],
258 nonempty := by norm_num
259}
260
261/-- Ground state probability for a two-level system. -/