DiscreteSystem
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.