harmonicOscillatorPartition
plain-language theorem explainer
Defines the closed-form partition function for a quantum harmonic oscillator with positive frequency omega at positive temperature T. Statistical mechanicians working in Recognition Science would cite this when extracting Planck's law or thermodynamic potentials from ledger-weighted sums. The definition is a direct algebraic encoding of the geometric series over levels E_n = (n + 1/2) hbar omega.
Claim. $Z = e^{-(1/(k_B T)) hbar omega / 2} / (1 - e^{-(1/(k_B T)) hbar omega})$ for frequency $omega > 0$ and temperature $T > 0$, with $hbar$ the RS-native reduced Planck constant.
background
The module derives the statistical mechanics partition function Z = sum exp(-beta E_i) as a sum over ledger configurations weighted by J-cost. Here beta is the inverse-temperature map supplied by the sibling beta definition, while hbar and tick come from Constants.RSNativeUnits and Constants.Codata. Upstream, CostAlgebra.H reparametrizes the Recognition Composition Law into the d'Alembert form H(xy) + H(x/y) = 2 H(x) H(y), which underpins the cost weighting used for energy levels.
proof idea
One-line definition that directly transcribes the standard geometric-series sum for the Boltzmann factors of the harmonic-oscillator spectrum E_n = (n + 1/2) hbar omega.
why it matters
Supplies the explicit oscillator Z that the module doc-comment states leads to Planck's radiation law, thereby connecting ledger sums to observable thermodynamics. It sits inside the broader THERMO-002 effort to obtain all thermodynamic potentials from RS-native constants (hbar = phi^{-5}, eight-tick phase-space discretization). No downstream uses are recorded yet, leaving open the question of how this Z feeds into freeEnergy or heatCapacity siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.