informationTheoryCert
plain-language theorem explainer
informationTheoryCert constructs a concrete instance of the InformationTheoryCert structure that certifies Shannon entropy axioms derived from the J-cost function in Recognition Science. It supplies the five-axiom count, zero minimum entropy at certainty, and strict positivity for uncertain outcomes. Information theorists or foundational physicists would cite it to link entropy to average J-cost over distributions. The definition is a direct record construction that references three upstream theorems for its fields.
Claim. The information theory certificate is the structure satisfying: the cardinality of the set of Shannon axioms equals 5, the J-cost of argument 1 equals 0, and for every real $r$ with $0 < r$ and $r ≠ 1$ the J-cost of $r$ is positive.
background
In the module Information Theory from RS, Shannon entropy is identified with the average J-cost of a probability distribution. The J-cost function satisfies Jcost 1 = 0 for certain outcomes and Jcost r > 0 for uncertain outcomes (0 < r ≠ 1). Shannon's five axioms (continuity, maximality, additivity, symmetry, subadditivity) are represented by the finite type ShannonAxiom whose cardinality is 5, corresponding to configDim D = 5 in the RS setting.
proof idea
The definition builds the InformationTheoryCert record by direct field assignment: five_axioms receives the value of shannonAxiomCount, min_H receives min_entropy, and pos_H receives pos_entropy. Each field is supplied by an upstream theorem (shannonAxiomCount by decide, min_entropy by Jcost_unit0, pos_entropy by Jcost_pos_of_ne_one).
why it matters
This definition supplies the certified interface that realizes the module claim linking Shannon entropy to the J-cost function as average cost. It encodes the five-axiom count as the RS counterpart to configDim D = 5 and bundles the non-negativity properties of entropy. No downstream uses are recorded, leaving open its application to capacity theorems or explicit entropy computations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.