StirlingApproximation
plain-language theorem explainer
StirlingApproximation encodes the combinatorial bound that the log of the multinomial coefficient for M trials across K outcomes satisfies log Omega <= M H(p) + K log M, with H the Shannon entropy. Researchers deriving thermodynamics from microstate counting under fixed J-cost would cite it to justify the entropy contribution to free energy. The declaration is a bare class definition that introduces the approximation as a structural hypothesis with no internal proof.
Claim. The Stirling approximation hypothesis states that for positive integers $K,M$ with $M>0$ and any probability vector $p$ on $K$ states with $p_i>0$ summing to 1, there exists a real number $log Omega >=0$ such that $log Omega <= M H(p) + K log M$, where $H(p)=-sum p_i log p_i$ is the Shannon entropy.
background
This declaration lives in the module that derives Shannon entropy from microstate counting under fixed average J-cost. The multinomial coefficient Omega(p) = M! / prod (M p_i)! counts the ways to realize distribution p; its logarithm is bounded above by M H(p) plus a K log M term. The recognition entropy function computes H(p). Upstream results include the cost algebra where H(x) = J(x) + 1 satisfies the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y), and the observer forcing that assigns J-cost to each recognition event.
proof idea
The declaration is a bare class definition packaging the inequality as a Prop. No lemmas are applied and the proof body is empty; the bound is posited as a structural hypothesis for the module's subsequent derivations of the Gibbs distribution.
why it matters
The hypothesis supplies the counting foundation that lets the module prove the Gibbs weights exp(-J/T_R) emerge from maximizing microstate multiplicity subject to fixed average J-cost. It supports the module claim that Shannon entropy is the quadratic shadow of J-cost and closes the backward direction from combinatorics to thermodynamics, complementing the forward minimization proved in MaxEntFromCost. It touches the finite-M tightness of the J-cost versus log-squared domination.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.