rateDistortionTheory
plain-language theorem explainer
Rate-distortion theory supplies the minimum rate R(D) required to keep distortion at or below a threshold D. Recognition Science workers cite it when deciding which ledger entries to drop according to their J-cost weight. The declaration is a direct string assignment that opens the Kolmogorov complexity discussion.
Claim. The rate-distortion function is defined by $R(D) = $ minimum achievable rate such that distortion remains at most $D$, where the minimum is taken over all compression schemes that respect the J-cost ordering of ledger entries.
background
The Information.Compression module derives data-compression bounds from J-cost rather than classical entropy alone. J-cost is the Recognition Science measure of ledger description length; lower J-cost corresponds to more organized, compressible information. The module first recalls Shannon's source-coding theorem (average code length at least H(X)) and then replaces the entropy bound with a J-cost minimization principle for lossy cases. Upstream structures supply the ledger factorization (DAlembert.LedgerFactorization) and the phi-forcing origin of J (PhiForcingDerived), while the dimensionless bridge K = φ^{1/2} appears in related constant derivations.
proof idea
One-line definition that assigns the descriptive string to rateDistortionTheory. No tactics or lemmas are applied; the body simply returns the literal text that anchors the subsequent Kolmogorov-complexity comments.
why it matters
The definition introduces the rate-distortion trade-off inside the J-cost framework of INFO-003, preparing the ground for later statements on lossless and lossy compression. It sits between the forcing-chain foundations (T5 J-uniqueness, T6 phi fixed point) and the concrete compression theorems that follow in the same module. No downstream uses are recorded yet, leaving open the question of an explicit R(D) formula expressed in phi-ladder units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.