Information Error Correction3 Deep From Jcost Err Corr3 Deep Cert

The certificate's scope

Error-correcting codes let a message survive noise: a sender adds redundant bits, and a receiver uses them to detect and fix mistakes. A standard bound on this ability is the Hamming bound, which says a code of length n with k message bits can correct at most t errors only if 2^(n-k) is at least the number of error patterns, the sum of binomial coefficients up to t. In the Recognition Science framework, a research note attached to this topic suggests that a particular cost value, J(phi), which equals about 0.118, might set a rate, and half of that, 0.059, an error fraction.

The machine-checked declaration ErrCorr3DeepCert, a certificate in the framework's library of formal theorems, does something much smaller. It packages three facts about a cost function, a measure of recognition effort. The cost is defined as J(m/e), where J(x) = (x + 1/x)/2 - 1. The certificate proves that this cost is zero when the two inputs are equal, that it is never negative when both inputs are positive, and that the number phi - 3/2 is positive. Here phi is the golden ratio, about 1.618, so this last fact simply states that phi is greater than 1.5.

The certificate's own documentation is explicit about its limits. It proves nothing specific to error correction, because the cost function is defined as J(m/e) without any reference to messages, errors, or codes. The Hamming bound and the suggested rate of 0.118 are a research note, a statement of where the idea was meant to go, not a result. What would turn this certificate into a theorem about its subject is a definition of m and e in the subject's own terms, a step the certificate does not take.

In plain terms, the certificate is a small, correct piece of groundwork. It verifies three elementary properties of a cost function and packages them into a reusable object. The leap from those properties to a statement about error-correcting codes remains unformalized and open. The certificate's value is that it pins down the foundation, not that it builds the house.

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)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The certificate does not prove the Hamming bound or any statement about error-correcting codes. The value 0.118 is a research note, not a derived or measured rate. The certificate does not establish that phi - 3/2 is the golden ratio's defining property, only that it is positive.

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/ErrorCorrection3DeepFromJCost.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: