max_entropy_uniform
plain-language theorem explainer
Maximum entropy for the uniform distribution over n positive outcomes equals the natural logarithm of n under the Shannon entropy definition. Information theorists and Recognition Science researchers would cite this when linking entropy to J-cost minimization over distributions. The tactic proof reduces the claim by unfolding the entropy and uniform definitions, invoking the logarithm quotient identity, and closing with field simplification followed by the ring tactic.
Claim. For any positive natural number $n$, the Shannon entropy $H = -p_1 log p_1 - ... - p_n log p_n$ of the uniform distribution (each $p_i = 1/n$) equals $log n$.
background
The module Information.ShannonEntropy derives Shannon entropy from Recognition Science J-cost. J-cost is given by $J(x) = (x + x^{-1})/2 - 1$, with the shifted form $H(x) = J(x) + 1 = (x + x^{-1})/2$ satisfying the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$ as stated in the CostAlgebra upstream definition. The uniform distribution assigns probability $1/n$ to each of $n$ outcomes; shannonEntropy applies the standard formula $-sum p_i log p_i$ to any probability distribution.
proof idea
The proof unfolds shannonEntropy and uniform, introduces positivity of $1/n$ via Nat.cast_pos, applies Real.log_div to obtain log(1/n) = -log n, reduces the scaled product via field_simp, and finishes with ring.
why it matters
This result is invoked directly by uniform_has_max_entropy in InformationIsLedger, which records IC-001.12: maximum entropy occurs for the uniform distribution and equates it to maximum information cost. It completes the INFO-001 derivation of Shannon entropy from J-cost structure in the paper Foundation of physics - Information theory from RS, placing the uniform case inside the broader forcing chain where entropy quantifies deviation from uniformity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.