Mathematics Information Theory From Rs

Information theory from Recognition Science

Information theory, as founded by Claude Shannon in 1948, measures the uncertainty in a set of possible outcomes. For a probability distribution p₁, p₂, ..., pₙ, the entropy H = -Σ pᵢ log pᵢ gives the average number of bits needed to describe an outcome. The theory rests on five axioms: continuity, maximality, additivity, symmetry, and subadditivity. These axioms ensure that entropy behaves as a sensible measure of information: it is continuous in the probabilities, maximal for the uniform distribution, additive for independent events, symmetric under relabeling, and subadditive when combining systems.

In Recognition Science, the framework models the same five axioms as a single inductive type with exactly five constructors. A machine-checked library of formal theorems proves that the cardinality of this type is 5, so the axiom count is not assumed but derived. The framework then identifies Shannon entropy with the average cost of recognition, where cost (the forced price of distinguishing one outcome from another) is given by the function J(x) = (x + 1/x)/2 - 1. This function is nonnegative, and it equals zero exactly at x = 1, which corresponds to a certain outcome. The library proves that J(1) = 0 and that J(r) > 0 for any r ≠ 1 with r > 0, so entropy is always nonnegative and vanishes only for certainty.

The framework establishes a certificate structure that bundles these results: the five axioms, the minimum entropy condition, and the positivity condition. This certificate is constructed from the underlying theorems, so the framework's information theory inherits the same proof discipline as its cost function. The signal-to-noise ratio in the Shannon capacity formula C = B × log₂(1 + S/N) is interpreted as the inverse of the cost function, so capacity per unit bandwidth becomes log₂(1 + J⁻¹(S/N)).

What this means in plain language: the framework does not introduce new axioms for information theory; it shows that Shannon's five axioms are exactly the structure needed, and that the entropy measure emerges from the same forced cost function that governs recognition. The nonnegativity of entropy is not assumed but proved from the cost function's properties. This gives a unified foundation where information, cost, and recognition all trace back to the same functional equation.

theorem shannonAxiomCount : Fintype.card ShannonAxiom = 5 := by decide

/-- Minimum entropy: J = 0 (certain outcome). -/
theorem min_entropy : Jcost 1 = 0 := Jcost_unit0

/-- Positive entropy: J > 0 (uncertain outcome). -/
theorem pos_entropy {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
    0 < Jcost r := Jcost_pos_of_ne_one r hr hne

def informationTheoryCert : InformationTheoryCert where
  five_axioms := shannonAxiomCount
  min_H := min_entropy
  pos_H := pos_entropy

What this page does not claim

The framework does not prove the Shannon capacity theorem C = B × log₂(1 + S/N); it only interprets the ratio S/N via the cost function. The framework does not derive the numerical value of entropy for any specific distribution; it establishes structural properties of the cost function. The five axioms are modeled as a type, not derived from the cost function; the derivation runs in the opposite direction.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/InformationTheoryFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: