twoLevel_gt_one
plain-language theorem explainer
The two-level partition function exceeds one for any real energy gap and positive temperature. Researchers deriving thermodynamic quantities from Recognition Science ledger sums would cite this bound when establishing positivity of free energy or entropy. The argument is a one-line wrapper that unfolds the definition and invokes positivity of the exponential.
Claim. For every real number $ε$ and every positive real temperature $T>0$, the two-level partition function satisfies $Z(ε,T)>1$.
background
In the Recognition Science derivation of statistical mechanics the partition function is obtained as a sum over ledger configurations weighted by J-cost. For the two-level system the explicit form is $Z=1+exp(-β ε)$ where $β$ denotes inverse temperature. The module THERMO-002 shows that free energy, average energy, entropy and heat capacity all follow from this $Z$ via the standard logarithmic derivatives.
proof idea
The proof is a one-line wrapper. It unfolds the definition of the two-level partition function, applies the lemma that the exponential is strictly positive, and finishes with linear arithmetic on the resulting inequality.
why it matters
This supplies the elementary positivity property needed for thermodynamic stability inside the Recognition Science ledger framework. It supports later derivations of free-energy and entropy bounds in the partition-function module before extension to general ledger sums. The result sits at the base of the T0-T8 forcing chain once the partition function is expressed in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.