uniform_has_max_entropy
plain-language theorem explainer
Uniform distributions over n outcomes achieve Shannon entropy exactly equal to log n. Researchers deriving information measures from the J-cost ledger in Recognition Science cite this to identify maximum uncertainty with maximum cost. The argument is a direct one-line application of the max_entropy_uniform lemma.
Claim. For every positive integer $n$, the Shannon entropy of the uniform probability distribution on $n$ outcomes equals $log n$.
background
The module develops the claim that information is the physical ledger: every recognition event is a ratio $x > 0$ carrying J-cost $J(x) = (x + x^{-1})/2 - 1$, with $J(1) = 0$ the unique balanced state. Shannon entropy is identified with expected J-cost, so the uniform distribution on $n$ outcomes realizes the maximum value $log n$. This sits inside the IC-001 sequence that equates information content with ledger imbalance and links to the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that applies the max_entropy_uniform lemma from the ShannonEntropy submodule.
why it matters
The result supplies IC-001.12, confirming that maximum entropy (hence maximum information cost) occurs precisely at the uniform distribution. It supports the module's unification of Shannon entropy with expected J-cost and the broader ledger interpretation of Wheeler's it-from-bit. No downstream uses are recorded yet, leaving open its insertion into entropy calculations for spectral emergence or inflaton potentials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.