Information Mutual Info2 From Jcost Mutual Info2 Cert

The certificate

In information theory, mutual information measures how much one random variable tells you about another. The classical definition, due to Claude Shannon in 1948, is I(X;Y) = H(X) + H(Y) − H(X,Y), where H denotes entropy. It answers a concrete question: if you learn the value of Y, how many bits of uncertainty about X disappear on average? The quantity is always nonnegative, and it is zero exactly when the two variables are independent.

The Recognition Science framework approaches this concept through its own primitive: a ledger, a discrete record of recognition events, and a forced cost, the unavoidable price of recording one event given another. The framework's central cost function is J(x) = (x + 1/x)/2 − 1, which its library proves is the unique function satisfying five plain conditions. A research note in the framework's machine-checked library of formal theorems proposes that at a special coupling value, mutual information equals J(phi) times the marginal entropy H(X), where phi is the golden ratio, giving I(X;Y) ≈ 0.118 × H(X). This is the idea the declaration MutualInfo2Cert was meant to support.

What the declaration itself actually establishes is far narrower. The machine-checked library defines a cost on a domain as J(m/e), the forced cost applied to a ratio of two real numbers. It then proves three general facts about this cost function: it vanishes when m equals e; it is nonnegative for positive inputs; and a certain threshold value, phi − 3/2, is positive. The declaration bundles these three facts into a structure called a certificate, and proves that such a certificate exists. These are the complete contents of the theorem.

The gap between the research note and the certificate is the definition of m and e. The certificate proves facts about a cost function applied to an arbitrary ratio of real numbers. It does not define m and e as anything related to mutual information, entropy, or recognition events. The note records where the idea was meant to go, not a result that has been reached. What would turn the certificate into a theorem about mutual information is a definition of m and e in that subject's own terms, which the library does not provide.

In plain language: the certificate proves three harmless facts about a cost function, and the mutual information claim remains an unproven research note. The framework's library is honest about this distinction. The certificate is a small but real piece of machine-checked mathematics; the leap to Shannon's quantity is a stated intention, not a derived result.

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]

theorem cert_inhabited : Nonempty MutualInfo2Cert := ⟨cert⟩

What this page does not claim

The certificate does not prove any statement about mutual information, entropy, or random variables. The research note's proposed equality I(X;Y) = 0.118 × H(X) is not a theorem. The certificate does not define m and e in terms of any information-theoretic quantity.

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