cert
plain-language theorem explainer
Packages three elementary facts about the RS domain cost and the canonical threshold into a single qubit-channel certificate. Anyone citing the RS claim that one qubit carries only φ⁻¹ classical bits after recognition overhead would point here for the structural side conditions. The body is a pure structure assembly: three already-proved lemmas are plugged into the three fields.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive arguments; and (iii) the canonical threshold is strictly positive.
background
The module treats qubit channel capacity in Recognition Science. Classically one qubit carries one bit; under RS the recognition overhead multiplies capacity by $\varphi^{-1}$, so the effective rate is about $0.618$ bits per qubit. The status line marks the development as a structural theorem (no sorry, no axioms).
The certificate structure QubitChannelCert packages three side conditions on a real-valued domain cost and a positive threshold. Domain cost is the local cost functional used to measure mismatch between measured and expected channel parameters; it is required to vanish when the two arguments agree and to stay nonnegative when both are positive. The canonical threshold is the positive cutoff against which capacity statements are compared.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: every recognition event has nonnegative J-cost. The three field lemmas assembled here are the in-module specializations of that positivity story to domain cost and the threshold.
proof idea
One-line structure construction. The three fields of the certificate are filled by the three sibling lemmas already proved in the same module: 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 a single named inhabitant of the qubit-channel certificate, so downstream capacity statements can assume the three side conditions by name rather than re-proving them. The module doc frames the target claim: RS quantum channel capacity equals $\varphi^{-1}$ times qubit count, the recognition overhead forced by the J-cost minimum and the golden-ratio fixed point (T5–T6 in the forcing chain). With no recorded used_by edges yet, this certificate is the structural anchor inside the information layer rather than a lemma consumed by a larger theorem. It closes the local packaging step for the structural (zero-sorry) qubit-capacity development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.