high_temp_limit
plain-language theorem explainer
High-temperature limit of ground-state probability reaches one half as beta approaches zero for any positive energy gap. Workers deriving statistical mechanics from Recognition Science's J-cost functional cite it to confirm the classical equipartition regime of the Boltzmann distribution. The argument rewrites the limit to the explicit value at beta equals zero then invokes continuity of the map beta to one over one plus exp of minus beta times gap.
Claim. For any gap > 0, let $P(beta) = 1 / (1 + exp(-beta * gap))$. Then the limit of $P(beta)$ as beta tends to 0 equals 1/2.
background
The module derives the Boltzmann distribution from Recognition Science's J-cost functional. Each state carries a recognition cost J(x); the cost-optimal allocation under a fixed total-cost constraint produces the exponential form with beta as Lagrange multiplier, yielding P_i = exp(-beta E_i) / Z. The ground-state probability for a two-level system with gap is the explicit function 1 / (1 + exp(-beta * gap)). This theorem treats the high-temperature regime where thermal energy greatly exceeds the gap, complementary to the low-temperature case where the ground state dominates.
proof idea
The tactic proof first rewrites the statement using the precomputed high_temp_value at beta equals zero. It unfolds groundStateProb and proves continuity of the map beta to 1 / (1 + exp(-beta * gap)) by showing the denominator is a continuous sum of the constant 1 and the composition of exp with a linear function. The final step applies the fact that a continuous function at a point has the required limit equal to its value there.
why it matters
This result closes the high-temperature case in the Recognition Science derivation of thermodynamics (THERMO-001). It confirms that the J-cost Boltzmann form recovers the classical equipartition limit, aligning with the framework's emergence of temperature from cost derivatives. No downstream uses are recorded, but the theorem pairs with the low-temperature limit noted in the module doc-comment to bracket the full temperature range.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.