surprisal
plain-language theorem explainer
Surprisal defines the information content of an outcome with probability p as -log p. Researchers deriving information measures from Recognition Science J-cost would cite it to connect classical surprisal to total cost minimization. The declaration is a one-line definition that directly encodes the standard formula.
Claim. For probability $p > 0$, the surprisal is defined by $I(p) := -log p$.
background
The ShannonEntropy module derives Shannon entropy from Recognition Science J-cost, where J(x) = ½(x + x^{-1}) - 1 quantifies recognition effort on probability ratios. Surprisal supplies the per-outcome information unit I(x) = -log(p(x)), with the module showing how total J-cost over a distribution yields the entropy expression. The setting follows the module insight that entropy measures deviation from uniformity via cost minimization. Upstream results include OptionAEmpiricalProgram.is establishing collision-free structure and SimplicialLedger.EdgeLengthFromPsi.is confirming algebraic tautologies in the ledger.
proof idea
This is a one-line definition that directly sets surprisal p hp to -Real.log p, matching the classical surprisal formula without further reduction.
why it matters
The definition feeds entropy_is_expected_surprisal, which states that entropy equals the expected surprisal, and shannon_equals_jcost, which equates Shannon entropy to total J-cost. This realizes the INFO-001 derivation that entropy emerges from J-cost minimization. It aligns with T5 J-uniqueness in the forcing chain by supplying the logarithmic term that matches the J-function form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.