cert
plain-language theorem explainer
Packages three elementary facts about the RS domain cost and the canonical threshold into a single HolevoBoundRS certificate. Anyone invoking the RS Holevo structure (chi_RS = phi^{-1} H_Shannon) cites this inhabited instance. The body is a pure field-wiring of three sibling lemmas already proved in-module.
Claim. There is a certificate that the RS domain cost satisfies $C(r,r)=0$ for every $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical Holevo threshold is strictly positive.
background
The module develops an RS reading of the Holevo bound: classical Holevo capacity obeys $\chi\le H(\text{ensemble})$, while RS inserts a recognition overhead so that $\chi_{\mathrm{RS}}=\varphi^{-1}H_{\mathrm{Shannon}}\approx 0.618,H$. Effective quantum information transmission is therefore a golden-ratio fraction of Shannon capacity.
HolevoBoundRS is the structure that packages the three algebraic side-conditions needed for that reading: the domain cost vanishes on the diagonal (equal measure and estimate), is nonnegative for positive arguments, and the canonical threshold is positive. The domain cost is the local cost functional on the recognition side; nonnegativity is the same J-cost positivity that appears in ObserverForcing (cost_nonneg: cost of any recognition event is nonnegative).
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge those three fields individually.
proof idea
One-line structure instance. The three fields of HolevoBoundRS are filled by the already-proved siblings domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further tactic work; the definition is pure wiring.
why it matters
Gives a concrete inhabited witness for the RS Holevo structure, so downstream code can treat the bound as a closed structural theorem (module status: 0 sorry, 0 axiom). The parent narrative is the RS Holevo claim $\chi_{\mathrm{RS}}=\varphi^{-1}H$, tying information capacity to the golden-ratio fixed point forced at T6 and to the J-cost calculus (T5). With used_by currently empty, this certificate is the local endpoint that makes the structure usable; the companion cert_inhabited likely just re-exports inhabitance. No open scaffold remains on this path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.