groundStateProb
plain-language theorem explainer
The ground state probability for a two-level system is given by the explicit formula 1/(1 + exp(-beta * gap)). Researchers deriving statistical mechanics from Recognition Science's J-cost functional cite this as the concrete expression for the lowest-energy occupation under cost-weighted selection. The definition is a direct one-line algebraic encoding of the normalized Boltzmann factor for energies 0 and gap.
Claim. For a two-level system with energy gap $g$ and inverse temperature $beta$, the ground-state occupation probability is $P_0 = 1/(1 + e^{-beta g})$.
background
The module derives the Boltzmann distribution from Recognition Science's J-cost functional, where each state carries a recognition cost J(x) = (x + x^{-1})/2 - 1. Lower-cost states are selected with higher probability under a fixed total-cost ledger constraint; the Lagrange multiplier for that constraint is identified with beta = 1/kT. Upstream, the probability def from QuantumLedger supplies the Born-rule amplitudes that become the weights, while gap defs from Gap45.Derivation and Masses.AnchorPolicy supply the phi-ladder energy differences.
proof idea
One-line definition that directly implements the two-level partition-function normalization: ground state at energy 0, excited state at energy gap, with the exponential Boltzmann factor taken from the J-cost maximization rule.
why it matters
Supplies the explicit ground-state probability used by the high-temperature limit (equal population at beta = 0) and low-temperature limit (ground-state dominance as beta to infinity) theorems in the same file. It realizes the key result P_i = exp(-beta E_i)/Z stated in the module's THERMO-001 derivation of statistical mechanics from J-cost, linking the forcing-chain self-similarity to thermodynamic limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.