pith. sign in
module module high

IndisputableMonolith.Mathematics.InformationTheoryFromRS

show as:
view Lean formalization →

This module derives core information theory objects from the Recognition Science J-cost function. It defines minimum entropy as the J=0 case for certain outcomes and introduces the Shannon axiom along with an information theory certificate. Researchers linking entropy to the forcing chain would cite it. The module consists entirely of definitions and axioms built on the Cost import.

claimThe module introduces the Shannon axiom, minimum entropy as $J=0$ for certain outcomes, positive entropy, and an information theory certificate, all expressed in terms of the J-cost from Recognition Science.

background

Recognition Science starts from the J-cost function J(x) = (x + x^{-1})/2 - 1 supplied by the upstream Cost module. This module extends that cost to information measures. It sets minimum entropy to the J=0 case when an outcome is certain and defines supporting objects such as the Shannon axiom and an information theory certificate. The local setting is the mathematics layer that prepares entropy for later use in the phi-ladder and forcing chain T0-T8.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the information-theoretic layer that connects J-cost to entropy concepts used in the Recognition framework. It feeds parent structures such as the mass formula and constant derivations that rely on the phi-ladder. It fills the step that relates minimum entropy to the J-uniqueness property in T5.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)