high_temp_value
plain-language theorem explainer
Ground state occupation probability equals one half exactly when inverse temperature vanishes. Researchers deriving the Boltzmann distribution from J-cost functionals cite this to anchor the high-temperature regime. The proof is a direct algebraic simplification after unfolding the definition of groundStateProb.
Claim. For any real gap parameter, the ground-state occupation probability at inverse temperature zero equals one half: $P_0(0) = 1/2$.
background
The module derives the Boltzmann distribution from Recognition Science's J-cost functional, where each state carries a recognition cost and the cost-optimal allocation under a fixed total cost constraint produces the exponential form with Lagrange multiplier beta. groundStateProb denotes the normalized occupation probability of the lowest energy level for a given gap, obtained from the partition function over the two states. The local setting treats temperature as emerging from the derivative of J-cost with respect to entropy, consistent with the core insight that lower-cost states are more probable.
proof idea
The proof is a one-line wrapper that unfolds the definition of groundStateProb, then applies simp followed by norm_num to reduce the expression at beta equal to zero to the numerical value one half.
why it matters
This supplies the base case for the high-temperature limit theorem in the same module, which shows the ground-state probability tends to one half as beta tends to zero. It forms part of the derivation of the Boltzmann distribution from J-cost in Recognition Science, matching the cost-weighted state selection in the module documentation and supporting the claim that states become equally populated at high temperature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.