jcost_uniform
plain-language theorem explainer
The theorem establishes that the J-cost assigned to a uniform distribution over n positive outcomes equals the natural logarithm of n. Information theorists working in the Recognition Science setting would cite this when showing that total J-cost recovers Shannon entropy. The proof is a one-line algebraic reduction that applies logarithm inversion and negation rules.
Claim. For any positive integer $n$, the J-cost of the uniform distribution with each outcome having probability $1/n$ satisfies $-log(1/n) = log n$.
background
The Information.ShannonEntropy module derives Shannon entropy from Recognition Science's J-cost structure. J-cost measures recognition effort on positive ratios via the formula J(x) = (x + 1/x)/2 - 1. Applied to a probability distribution, the sum of J-cost terms over the probabilities yields the entropy value, with the uniform distribution serving as the maximum-entropy reference case.
proof idea
The proof is a one-line wrapper that rewrites the left-hand side by replacing the reciprocal, applying the logarithm-of-inverse identity, and canceling the resulting negation.
why it matters
This identity supplies the uniform-distribution base case needed to equate total J-cost with Shannon entropy in the module's derivation. It supports the core claim that entropy emerges directly from J-cost minimization over distributions, consistent with the module target of recovering information measures from the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.