QCap4DeepCert
plain-language theorem explainer
Certificate structure bundling three properties used in the RS quantum-capacity development: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code builds a concrete inhabited instance from the matching lemmas. Pure structural packaging with no proof body.
Claim. A certificate record asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical recognition threshold is strictly positive.
background
The Information module develops an RS reading of quantum channel capacity. Classically one writes $Q = \max_{\phi_A} I(A;B)$; here the claim is that at the canonical recognition coupling one has $Q = J(\phi)^{-1}$ times the classical capacity, with $J$ the unique cost forced by the Recognition Composition Law.
Domain cost is the bivariate cost used on measurement/estimate pairs in this module. The first field requires it to vanish when the two arguments agree (and are nonzero), i.e. perfect match carries zero recognition cost. The second field is the usual nonnegativity of cost for positive inputs, aligning with the foundation fact that every recognition event has nonnegative cost (via $J$-cost nonnegativity). The third field only asks that the module's canonical threshold be strictly positive, so capacity scalings that divide by it are well-defined.
proof idea
Definitional structure only: three named fields, no constructors beyond the record, no tactics. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named interface for the three cost/threshold facts the RS quantum-capacity story needs before quoting $Q = J(\phi)^{-1}\cdot C_{\mathrm{classical}}$. Downstream, cert assembles a concrete value and cert_inhabited records Nonempty of this type, so later lemmas can assume a certificate without re-proving the three bullets. Ties the Information layer to foundation cost nonnegativity and to the $J$/phi landmarks (T5–T6) that fix the capacity prefactor. Does not itself derive the capacity identity; it only packages the structural hypotheses that identity will rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.