DiscreteSystem
plain-language theorem explainer
A discrete system consists of a positive number of energy levels, each carrying a real energy value and a positive integer degeneracy. It supplies the finite data structure required to define the partition function and derived thermodynamic quantities in Recognition Science. The declaration is a structure definition that encodes the level count, maps, and two positivity constraints with no further lemmas.
Claim. A discrete system consists of a positive integer $N$, a map $E : [N] → ℝ$ assigning energies to levels, a map $g : [N] → ℕ$ with $g_i ≥ 1$ for each level, and the requirement $N > 0$.
background
The module derives the partition function from ledger sums weighted by J-cost. Energy is the native alias for real numbers. Upstream LedgerFactorization.of supplies the structure of (ℝ₊, ×) and J calibration. Canonical arithmetic from ArithmeticOf supplies the initial Peano object used in counting levels.
proof idea
Structure definition that directly packages numLevels, energy map, degeneracy map, and the two positivity fields. No lemmas or tactics are invoked.
why it matters
It is the input type for partitionFunction, freeEnergy, averageEnergy, entropy, and heatCapacity. The declaration supplies the discrete levels needed for the ledger-based derivation of Z in the THERMO-002 setting. It connects the finite-sum construction to the Recognition Science claim that thermodynamic potentials emerge from J-cost sums.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.