lossyCompression
plain-language theorem explainer
Lossy compression is defined as approximate reconstruction that accepts distortion, permitting rates below the entropy H(X). Information theorists and Recognition Science researchers cite it when modeling which ledger data to discard based on J-cost importance. The definition is a direct string assignment accompanied by a rate-distortion comment.
Claim. Lossy compression is approximate reconstruction accepting distortion $D$, with rate $R(D)$ the minimum rate such that distortion is at most $D$. In Recognition Science this corresponds to discarding high J-cost information while allowing the compressed representation to have lower total J-cost than a faithful copy.
background
The module INFO-003 derives fundamental limits on data compression from J-cost. Shannon's source coding theorem states that average code length is at least the entropy $H(X) = -∑ p(x) log₂ p(x)$, and no lossless scheme can beat this bound. In Recognition Science, information carries J-cost; compressed forms have lower J-cost because they are more organized, so the entropy limit equals the minimum J-cost for faithful representation and compression equals J-cost minimization.
proof idea
This is a definition that directly assigns the string description of lossy compression together with an attached explanatory comment on rate-distortion trade-offs.
why it matters
The definition supplies the lossy counterpart to the lossless case treated by source_coding_theorem in the same module. It completes the picture that compression in Recognition Science is J-cost minimization, allowing rates below H(X) when high-J-cost ledger entries are discarded. It sits inside the broader derivation of compression limits from the J-cost function introduced in the Cost and ObserverForcing modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.