IndisputableMonolith.Information.MutualInfo2FromJCost
Defines a two-variable mutual-information certificate built from the RS J-cost on positive reals, together with a domain cost, a canonical positive threshold, and nonnegativity lemmas. Information theorists working in the Recognition stack would cite it when mutual information must be expressed as a J-cost defect rather than Shannon entropy. The module is mostly definitional: it packages the cost, threshold, and an inhabited certificate structure.
claimOn positive reals, a domain cost $C$ is induced from the RS cost $J(x)=(x+x^{-1})/2-1$. A canonical threshold $\theta>0$ is fixed. A two-variable mutual-information certificate is a structure asserting that the mutual information of a pair is controlled by $C$ relative to $\theta$, with nonnegativity $C\ge 0$ and evaluation-at-equality identities.
background
Recognition Science measures discrepancy by the unique symmetric cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced by the Recognition Composition Law. The Cost import supplies that $J$ and its elementary identities; Constants supplies the RS tick scale used elsewhere in the stack.
This module sits in the Information domain. It lifts $J$ to a domain cost on positive quantities (the sibling domainCost), records that the cost vanishes at equality and is nonnegative, and introduces a strictly positive canonical threshold against which mutual-information defects are compared.
The main packaged object is a two-variable mutual-information certificate: a Prop-carrying structure that ties a pair's mutual information to the domain cost and the threshold, so downstream arguments can treat MI as a $J$-cost defect rather than a Shannon functional.
proof idea
Definition module with short supporting lemmas, not a deep proof development. Domain cost is defined by applying $J$ (from Cost) to a positive ratio or scale; equality and nonnegativity are immediate from the corresponding properties of $J$. The canonical threshold is a positive constant (positivity is a one-line lemma). The mutual-information certificate is a structure bundling the cost/threshold data; inhabitation is witnessed by a concrete default certificate constructor.
why it matters in Recognition Science
Gives the Information layer a native RS handle on two-variable mutual information: MI is read as a $J$-cost defect above a fixed positive threshold, not as an independent Shannon primitive. That keeps information inequalities inside the same cost calculus that forces $J$-uniqueness (T5), $\phi$, and the eight-tick octave elsewhere in the monolith.
No downstream edges are recorded yet in the mirror graph, so this module is a leaf provider: later MI bounds, channel lemmas, or recognition-capacity arguments are expected to import the certificate and the domain-cost nonnegativity facts rather than re-derive them from $J$.
scope and limits
- Does not define Shannon entropy or classical KL divergence.
- Does not prove data-processing or chain-rule identities for mutual information.
- Does not treat $n$-variable mutual information for $n>2$.
- Does not connect the certificate to physical constants ($c$, $\hbar$, $\alpha$) or mass rungs.
- Does not claim uniqueness of the canonical threshold beyond positivity.