DiscreteSystem
DiscreteSystem supplies the finite energy spectrum required to compute the partition function Z as a sum over levels in the Recognition Science thermodynamics module. It is cited by the definitions of free energy, average energy, entropy, and heat capacity. The structure is introduced directly as a record with built-in positivity invariants on level count and degeneracies.
claimA discrete system consists of a positive integer $N$, a map assigning real energies $E_i$ to each of the $N$ levels, and a map assigning positive integer degeneracies $g_i$ with $g_i$ at least 1 for every level.
background
The module derives the partition function from RS ledger structure, where Z encodes thermodynamic quantities via sums weighted by J-cost. DiscreteSystem abstracts a finite collection of energy levels with degeneracies. Upstream, the Energy type is the native real, and ledger factorization provides the underlying discrete configurations. Canonical arithmetic objects from the foundation supply the natural-number indices and positivity constraints.
proof idea
The declaration is a pure structure definition introducing the type and its fields without further computation or proof obligations beyond the stated invariants.
why it matters in Recognition Science
It serves as the common input type for the thermodynamic functions that recover standard relations such as F = -k_B T ln Z and S = k_B (ln Z + β ⟨E⟩). This realizes the THERMO-002 goal of expressing the partition function from ledger sums. It bridges the foundation's arithmetic and ledger objects to statistical mechanics.
scope and limits
- Does not specify the origin of the energy values in terms of J-cost.
- Does not handle the continuous or infinite-level limit.
- Does not include any dynamics or time evolution.
- Does not constrain the spacing of energy levels.
- Does not incorporate the phi-ladder or specific RS constants.
formal statement (Lean)
42structure DiscreteSystem where
43 /-- Number of energy levels -/
44 numLevels : ℕ
45 /-- Energy of each level -/
46 energy : Fin numLevels → ℝ
47 /-- Degeneracy of each level (must be positive) -/
48 degeneracy : Fin numLevels → ℕ
49 /-- At least one level -/
50 nonempty : numLevels > 0
51 /-- Each level has degeneracy ≥ 1 -/
52 deg_pos : ∀ i, degeneracy i ≥ 1
53
54/-- The canonical partition function Z = Σᵢ gᵢ exp(-βEᵢ). -/