cert
plain-language theorem explainer
Packages the three elementary facts needed for the Shannon-capacity-from-J-cost certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical SNR threshold is positive. Anyone citing the structural channel-capacity claim in this module will pull this bundle. The body is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that the domain cost $D(m,e)$ satisfies $D(r,r)=0$ for all $r\neq 0$, $D(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
This module derives a Shannon channel-capacity identity from the Recognition Science J-cost. In RS-native units the classical formula $C=B\log_2(1+\mathrm{SNR})$ is evaluated at the forced SNR $J(\varphi)^{-2}\approx 71.7$, yielding $C\approx B\cdot 6.18$ bits/s/Hz, structurally near $\varphi^{2\varphi}$.
The domain cost $D(m,e)$ is the local mismatch functional built from the J-cost $J(x)=(x+x^{-1})/2-1$. The certificate structure demands three elementary properties of $D$ and of the canonical threshold $T$ (the positive SNR scale at which capacity is read off). Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: every recognition event has cost $\ge 0$ because $J$ itself is nonnegative on $(0,\infty)$.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (positivity of the threshold). No additional algebra is performed here.
why it matters
Gives a single named inhabitant of the channel-capacity certificate so downstream arguments can assume the three cost/threshold axioms without re-proving them. The module is marked structural (0 sorry, 0 axiom) and sits in the information layer that links J-cost uniqueness (forcing chain T5) and the golden ratio fixed point (T6) to a concrete Shannon figure of merit. No used-by edges are recorded yet; the natural consumer is any theorem that quotes the $C=B\log_2(1+\mathrm{SNR})$ evaluation at the RS SNR.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.