def
definition
def or abbrev
summary
show as:
view Lean formalization →
formal statement (Lean)
229def summary : List String := [
proof body
Definition body.
230 "Compression limit = entropy H(X)",
231 "Compression = J-cost minimization",
232 "Entropy = minimum J-cost for faithful representation",
233 "Redundancy = removable excess J-cost",
234 "Random data already at minimum J-cost"
235]
236
237/-! ## Falsification Criteria -/
238
239/-- The derivation would be falsified if:
240 1. Compression below entropy achieved
241 2. J-cost doesn't decrease with compression
242 3. Random data can be systematically compressed -/