shannonAxiomCount
plain-language theorem explainer
The theorem verifies that the inductive encoding of Shannon's entropy axioms contains precisely five elements. Information theorists extending Recognition Science to information measures would cite this to align the axiom count with the classical Shannon set. The proof is a direct decision procedure that calculates the finite cardinality from the inductive definition's constructors.
Claim. The cardinality of the finite type of Shannon axioms is five, where the axioms are continuity, maximality, additivity, symmetry, and subadditivity: $|$ShannonAxiom$| = 5$.
background
The module encodes Shannon entropy as the average J-cost of a probability distribution, matching the classical formula H = -Σ p_i log p_i. Shannon's axioms are represented by the inductive type with five constructors: continuity, maximality, additivity, symmetry, subadditivity. This count is asserted to equal the configuration dimension D = 5.
proof idea
The proof is a one-line wrapper invoking the decide tactic on the equality Fintype.card ShannonAxiom = 5. The tactic succeeds by enumerating the five constructors of the inductive type ShannonAxiom, which derives the necessary Fintype instance.
why it matters
This declaration provides the five_axioms field in the InformationTheoryCert structure, which bundles the axiom count with minimum and positive entropy properties. It fills the module's claim that the five Shannon axioms correspond to configDim D = 5 in the RS framework. The result supports deriving information theory from the J-cost functional without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.