ChannelCap2Cert
plain-language theorem explainer
Certificate structure bundling three analytic facts needed for the Shannon capacity-from-J-cost derivation: diagonal domain cost vanishes, domain cost is nonnegative on the positive quadrant, and the canonical SNR threshold is positive. Downstream code inhabits it once and uses Nonempty as a structural witness. Pure definition; no proof obligations live here.
Claim. A channel-capacity certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold (the RS SNR scale $J(\varphi)^{-2}$) is strictly positive.
background
The module derives Shannon channel capacity $C = B \log_2(1+\mathrm{SNR})$ in Recognition Science units. The structural claim is that at the forced SNR scale $\mathrm{SNR}=J(\varphi)^{-2}\approx 71.7$ one obtains $C=B\log_2(72.7)\approx B\cdot 6.18$ bits/s/Hz, numerically near $\varphi^{2\varphi}$.
Domain cost is the two-argument cost used on the measurement/error pair $(m,e)$; the certificate requires it to vanish on the diagonal $m=e\neq 0$ and to stay nonnegative for positive arguments. Those properties mirror the global J-cost nonnegativity theorem (cost of any recognition event is $\ge 0$, via $J$-cost nonnegativity at positive state). Canonical threshold is the positive real that pins the RS operating SNR.
Local status is structural: zero sorry, zero axiom. The certificate is the Prop-bundle that later definitions inhabit rather than a capacity formula itself.
proof idea
No proof body: this is a structure declaration. The three fields are pure propositions (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the module a single named witness type for the analytic hypotheses behind the J-cost channel-capacity claim. Downstream, cert builds a concrete inhabitant and cert_inhabited packages Nonempty ChannelCap2Cert, so later lemmas can assume the bundle rather than restate three separate facts.
Sits in the information layer that connects the forced J-cost (T5 uniqueness, RCL) to a Shannon figure of merit at the $\varphi$-native SNR. The module doc frames the numerical target $C/B\approx 6.18\sim\varphi^{2\varphi}$ as structural, not fitted. The certificate does not itself compute capacity; it is the gate that lets the structural theorem cite cost geometry cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.