cert
plain-language theorem explainer
Packages three elementary facts about the recognition domain cost into a single certificate: diagonal vanishing, nonnegativity on the positive quadrant, and a strictly positive canonical threshold. Anyone citing the RS quantum-capacity structural layer uses this witness. The body is a pure structure instance that wires three sibling lemmas into the certificate fields.
Claim. There is a certificate asserting: (i) the domain cost of equal positive measure and evidence vanishes, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical recognition threshold is strictly positive.
background
The module develops the Recognition Science account of quantum channel capacity. Classically one writes $Q=\max_{\phi_A} I(A;B)$; in RS the same quantity is identified with $J(\phi)^{-1}$ times classical capacity at the canonical recognition coupling, where $J$ is the unique cost forced by the Recognition Composition Law (T5).
Domain cost $C(m,e)$ is the local cost assigned to a measure/evidence pair on the recognition side. The certificate structure collects the three elementary properties needed downstream: vanishing on the diagonal $m=e$, nonnegativity for positive arguments, and positivity of the canonical threshold that sets the recognition coupling scale.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity on positive states. The present certificate specializes that fact to the domain-cost presentation used by the information layer.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas that already prove diagonal vanishing of domain cost, nonnegativity of domain cost on the positive quadrant, and positivity of the canonical threshold. No new arithmetic is performed.
why it matters
Gives an inhabited certificate object for the structural quantum-capacity layer of RS Information (session 3). The module status is a structural theorem with zero sorry and zero axioms; this definition is the concrete witness that the three cost/threshold hypotheses hold for the domain-cost model. It sits under the RS claim $Q=J(\phi)^{-1}\cdot$ classical capacity at the canonical coupling, which itself rests on T5 $J$-uniqueness and the forced golden ratio $\phi$ (T6). No downstream consumers are recorded yet; the natural parent is any theorem that assumes the certificate structure rather than the three raw lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.