InformationTheoryCert
plain-language theorem explainer
This structure packages a certificate that the J-cost function satisfies Shannon's five axioms together with non-negativity at unity and strict positivity elsewhere. Researchers deriving information theory from Recognition Science would cite it to confirm that entropy axioms follow from the RS cost function without additional assumptions. The declaration is a direct structure bundling the axiom cardinality, the zero at r=1, and the positivity predicate.
Claim. The structure asserts that the set of Shannon axioms has cardinality five, that the J-cost satisfies $J(1)=0$, and that $J(r)>0$ for every real $r>0$ with $r≠1$.
background
The module derives information theory from Recognition Science by identifying Shannon entropy with the average J-cost of a probability distribution. J-cost is the function imported from Cost, given explicitly by $J(x)=(x+x^{-1})/2-1$ (equivalently cosh(log x)-1). ShannonAxiom is the inductive type whose five constructors are continuity, maximality, additivity, symmetry and subadditivity; its Fintype instance supplies the cardinality used in the first field.
proof idea
The declaration is a structure definition with no proof body. It simply declares the three fields whose values are supplied later by the sibling definitions shannonAxiomCount, min_entropy and pos_entropy.
why it matters
The structure supplies the type that informationTheoryCert inhabits, thereby certifying that the five Shannon axioms hold for J-cost and that entropy is non-negative. This step closes the link between the Recognition Science forcing chain (T5 J-uniqueness) and information theory, confirming that configDim D=5 matches the axiom count and that H≥0 follows from J≥0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.