boltzmannFactor_pos
plain-language theorem explainer
The lemma establishes that the Boltzmann factor for any energy level with positive degeneracy is strictly positive for any real beta. Researchers deriving the partition function and normalized probabilities in Recognition Science statistical mechanics would cite it. The proof is a direct term-mode reduction that unfolds the factor definition and applies multiplication positivity to the cast degeneracy and the exponential.
Claim. Let $E$ be an energy level with degeneracy $d > 0$ and energy value $E$. For any real number $beta$, the Boltzmann factor $d · exp(-beta · E) > 0$.
background
The module derives the Boltzmann distribution from Recognition Science J-cost, where lower-cost states are selected under a fixed ledger constraint and beta emerges as the Lagrange multiplier conjugate to total cost. An EnergyLevel is a structure pairing a real energy value with a natural-number degeneracy that is required to be positive. The Boltzmann factor itself is the product of this degeneracy (cast to reals) and exp(-beta times energy), consistent with the exponential form appearing in upstream chemistry definitions of activation-energy factors.
proof idea
Term-mode proof that unfolds boltzmannFactor then applies mul_pos. The first subgoal is discharged by Nat.cast_pos.mpr on the deg_pos field of the EnergyLevel structure; the second subgoal is discharged by exp_pos.
why it matters
The result is invoked by the downstream theorem partition_positive to guarantee that the sum defining the partition function remains positive when beta > 0. It supplies the elementary positivity step required for the THERMO-001 derivation of P_i = exp(-beta E_i)/Z from J-cost, ensuring the normalizing constant is well-defined and the probabilities are non-negative before any further thermodynamic limits are taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.