Information Compression3 Deep From Jcost Data Compr3 Deep Cert

The certification record

In information theory, the optimal average length of a compressed message is bounded below by the source's entropy, H, measured in bits per symbol. A code that achieves this bound is called optimal. The Recognition Science framework adds a cost term to this picture: it models the overhead of a recognition event, a discrete record of a comparison, as a function J of the ratio between two quantities.

The machine-checked library of formal theorems contains a structure named DataCompr3DeepCert. The structure bundles three proven facts about the cost function domainCost, defined as J(m/e) for real numbers m and e. First, when the two inputs are equal, the cost is zero. Second, for positive inputs, the cost is never negative. Third, a particular constant, phi minus 3/2, is positive. Each of these is a theorem in the library, verified by the kernel.

The declaration itself is a certificate: it packages these three facts into a single object, and the library proves that such a certificate exists. What the certificate does not do is say anything about data compression in particular. The cost function is defined without any reference to messages, sources, or codes. The docstring records that the module was meant to be about compression, but the theorems hold for any positive real numbers m and e. The research note mentions an overhead of J(phi) bits per symbol, roughly 0.118 bits, but that claim is not part of the certificate.

In Recognition Science, the framework's library proves general facts about J, and this certificate is a small instance. The honest reading is that the certificate establishes three properties of a cost formula, not a result about compression. A theorem about compression would need a definition of m and e in terms of a source and its encoding. That definition is absent here, so the certificate remains a template, not an applied result.

structure DataCompr3DeepCert where
  cost_at_eq : ∀ r : ℝ, r ≠ 0 → domainCost r r = 0
  cost_nonneg : ∀ m e : ℝ, 0 < m → 0 < e → 0 ≤ domainCost m e
  threshold_pos : 0 < canonicalThreshold

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

structure DataCompr3DeepCert where
  cost_at_eq : ∀ r : ℝ, r ≠ 0 → domainCost r r = 0
  cost_nonneg : ∀ m e : ℝ, 0 < m → 0 < e → 0 ≤ domainCost m e
  threshold_pos : 0 < canonicalThreshold

What this page does not claim

The certificate does not prove that any particular code achieves a length of H plus 0.118 bits per symbol. The certificate does not define what m and e mean for a data source or a compression algorithm. The certificate does not establish that J(phi) is the correct overhead for any real-world compression task.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/Compression3DeepFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: