twoLevel_at_zero
plain-language theorem explainer
The declaration shows that the two-level partition function with zero energy separation equals 2 for any positive temperature T. Researchers deriving thermodynamic quantities from Recognition Science ledger sums would reference this degenerate case. The proof reduces directly via unfolding the partition definition and applying zero-product and exponential identities.
Claim. For any real number $T > 0$, the partition function $Z$ of a two-level system with energy gap $ε = 0$ satisfies $Z = 2$.
background
The module derives the statistical mechanics partition function from the Recognition Science ledger structure, where $Z = Σ exp(-β E_i)$ encodes free energy, average energy, and entropy. Beta denotes the inverse temperature factor. The two-level partition function specializes this sum to two states separated by energy epsilon, with the zero-gap case yielding degeneracy of 2.
proof idea
The proof unfolds the twoLevelPartition definition incorporating the beta factor. It then applies the mul_zero lemma from arithmetic foundations together with the exp_zero identity, followed by ring normalization to obtain equality with 2.
why it matters
This supplies the zero-gap base case for two-level systems in partition function derivations from ledger sums. It aligns with the core module insight that Z emerges as a weighted sum over ledger configurations, consistent with the forcing chain from T0 to T8 and the Recognition Composition Law. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.