holevo_bound
plain-language theorem explainer
Intended claim: classical capacity of a quantum channel is at most the Holevo quantity χ = S(ρ) − Σ p_x S(ρ_x) (von Neumann entropy). Formally the Lean statement is ⊤, proved by trivial. Cite only as a named placeholder in the INFO-002 channel-capacity module; no quantitative bound is checked.
Claim. Intended content: the classical capacity $C$ of a quantum channel satisfies $C \le \chi$, where the Holevo information is $\chi = S(\rho) - \sum_x p_x S(\rho_x)$ and $S$ is von Neumann entropy. The formalized statement is simply $\top$.
background
Module INFO-002 aims to derive Shannon channel capacity from Recognition Science ledger bandwidth: $C = \max_{p(x)} I(X;Y)$ bits per use, with the Gaussian special case $\tfrac12\log_2(1+S/N)$. Capacity is read as the ledger's fundamental record/transmit rate.
Sibling material defines a discrete memoryless Channel (input/output alphabet sizes and transition kernel $P(y|x)$), mutual information, and classical capacity as a max of $I(X;Y)$. The Holevo bound is the standard quantum upgrade: classical messages encoded in states $\rho_x$ with prior $p_x$ cannot exceed $\chi = S(\rho)-\sum_x p_x S(\rho_x)$ with $\rho=\sum_x p_x\rho_x$.
Upstream graph edges touch horizon area $A=4\ell_P^2 S$ (Bekenstein–Hawking reading) and a $\phi$-power density ladder; those are ambient RS imports, not ingredients of this proof.
proof idea
Term proof of True by trivial. No lemmas on von Neumann entropy, ensembles, or channel composition are applied. The declaration is a named stub whose mathematical content lives only in the doc-comment.
why it matters
Marks the quantum-capacity slot next to classical siblings (shannons_theorem, capacity_from_ledger, mutual_info_bounded) under the ledger-bandwidth program. In RS, information rates ultimately sit on ledger tick structure (eight-tick octave, $\phi$-scaled constants); Holevo is the natural quantum ceiling once channels are promoted beyond classical DMC.
Nothing downstream depends on it yet (used_by empty). It does not close a forcing-chain step (T0–T8) and does not constrain $\alpha$, masses, or $D=3$. It records intent to bound quantum classical-capacity by $\chi$ inside the same module that already treats Shannon capacity as ledger-limited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.