ShannonAxiom
plain-language theorem explainer
ShannonAxiom enumerates the five classical properties of entropy as an inductive type with constructors continuity, maximality, additivity, symmetry, and subadditivity. Information theorists deriving entropy from Recognition Science cost functions cite it to equate the axiom count with configuration dimension D = 5. The definition carries no proof body; Lean derives DecidableEq, Repr, BEq, and Fintype instances automatically to support downstream cardinality checks.
Claim. The Shannon axioms are the five properties of the entropy functional: continuity, maximality, additivity, symmetry, and subadditivity.
background
In Recognition Science, Shannon entropy H equals the average J-cost of a probability distribution, where J-cost is the function J(r) = (r + r^{-1})/2 - 1. The module InformationTheoryFromRS encodes classical information theory directly from this cost function, with H ≥ 0 following from J ≥ 0. Shannon's five axioms are listed explicitly as the constructors of an inductive type whose cardinality is asserted to equal the configuration dimension D = 5.
proof idea
The declaration is an inductive definition that introduces exactly five constructors. Deriving DecidableEq, Repr, BEq, and Fintype is performed automatically by Lean; no tactics or lemmas are applied inside the body.
why it matters
The definition supplies the axiom enumeration required by InformationTheoryCert, which records five_axioms : Fintype.card ShannonAxiom = 5 together with the statements min_H : Jcost 1 = 0 and pos_H : 0 < Jcost r for r ≠ 1. It realizes the module claim that the five axioms correspond to configDim D = 5 and closes the interface between classical information theory and the RS forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.