Information Mutual Info2 From Jcost

Mutual information at the recognition coupling

Mutual information is a classical quantity from information theory: it tells you how much knowing one variable reduces your uncertainty about another. For two variables X and Y, it is written I(X;Y) = H(X) + H(Y) - H(X,Y), where H is the Shannon entropy. The value is zero when the variables are independent, and it grows as they become more correlated. A common way to think of it is the amount of information they share, the overlap between two streams of data.

In the Recognition Science framework, the idea is to express this shared information using the framework's cost function. The cost function J(x) = (x + 1/x)/2 - 1 measures the price of a recognition event, and it is zero when the two sides are equal. The framework defines a domain cost as J applied to a ratio of two quantities, m and e. The three facts it proves are that this cost is zero when m equals e, that it is never negative for positive inputs, and that a certain threshold value, phi minus 3/2, is positive. These are general properties of the cost function, not specific claims about any particular information source.

The research note attached to the framework goes further: it proposes that at the recognition coupling J(phi), the mutual information equals J(phi) times the marginal entropy H(X), which is about 0.118 times H(X). This would mean that at a special point, the shared information is a fixed fraction of the total entropy. But this is a research note, not a proved result. The framework itself proves only the three general facts about the cost function, and it explicitly states that it proves nothing specific to this subject, because the quantities m and e are not defined in terms of any particular information source.

In plain language, the framework establishes a small but clean foundation. It shows that the cost-based measure behaves sensibly: it is zero when the two sides match, it never goes negative, and a key threshold is positive. The larger claim about mutual information being a fixed fraction of entropy remains a target, not a proved theorem. The framework is a template, a set of tools waiting for a definition of m and e that would make it a real theorem about information.

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]

What this page does not claim

The framework does not prove that mutual information equals a fixed fraction of entropy. The framework does not define m and e in terms of any specific information source.

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: