CompressionFalsifier
plain-language theorem explainer
The CompressionFalsifier structure enumerates three propositions whose truth would contradict the Recognition Science derivation of compression bounds from J-cost, together with an implication showing that the first yields falsehood. Researchers checking consistency between J-cost minimization and Shannon theory would cite the definition when stating empirical test conditions. It is introduced as a bare structure definition with no attached proof obligations.
Claim. A record consisting of propositions $B$, $J$, $R$ and a map $f:B→⊥$, where $B$ asserts that some compression scheme achieves average code length strictly below Shannon entropy, $J$ asserts that J-cost fails to decrease under compression, and $R$ asserts that random data admits systematic compression.
background
The Information.Compression module derives fundamental limits on data compression from the J-cost functional introduced in the Cost module. Shannon entropy supplies the classical lower bound: average code length is at least $H(X)=-∑p(x)log₂p(x)$. Recognition Science equates this bound with the minimum J-cost of a faithful representation, so that any compression step corresponds to a reduction in J-cost.
proof idea
This is a pure structure definition containing no proof body or tactics. It simply packages the three falsifying propositions and the implication from the entropy-violation proposition to falsehood.
why it matters
The definition supplies the explicit falsification interface for the INFO-003 claim that J-cost minimization recovers the source coding theorem. It sits downstream of the J-cost and ShannonEntropy modules. No downstream theorems are recorded, leaving open whether the three conditions can be shown mutually contradictory inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.