Pith. sign in
module module moderate

IndisputableMonolith.Information.Channel_Capacity_Qubit_RS

show as:
view Lean formalization →

Module packaging a Recognition-Science certificate for qubit channel capacity: a nonnegative domain cost, a positive canonical threshold, and an inhabited certificate record tying them together. Information theorists working in RS units would cite the certificate when bounding one-shot or discrete-time qubit channels against the J-cost. The file is mostly definitions and elementary positivity lemmas, not a deep capacity theorem.

claimIn RS units, a qubit channel is assigned a nonnegative domain cost $C$ and a positive canonical threshold $\theta>0$. A qubit-channel certificate is a record asserting that the channel's cost data meet the threshold constraints used for capacity bookkeeping; such a certificate is inhabited.

background

Recognition Science measures recognition effort by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), developed in the Cost import and forced unique by the T5 step of the unified forcing chain. Constants supplies the RS time quantum $\tau_0=1$ tick, so discrete channel uses are counted in integer ticks rather than continuous Shannon time.

This module sits in the Information domain and introduces a domain cost functional together with a canonical numerical threshold against which qubit-scale channels are scored. The cost is required to be nonnegative; the threshold is required to be strictly positive. Those two facts are the only analytic content beyond the certificate record itself.

No full Holevo or Shannon capacity formula is derived here. The objects are bookkeeping hooks so later RS information lemmas can compare a qubit channel's recognition cost to the forced $\phi$-ladder and eight-tick octave scales without reopening the Cost development.

proof idea

Definition module with light lemma support. Domain cost is introduced as a function; equality-at-a-point and nonnegativity are recorded as short lemmas. Canonical threshold is a positive constant (positivity lemma immediate from the defining expression). QubitChannelCert is a structure bundling the cost/threshold data; an explicit inhabitant cert is built, and cert_inhabited packages that construction. No multi-step tactic proofs or capacity inequalities appear.

why it matters in Recognition Science

Gives the Information layer a named, inhabited certificate type for qubit channels so downstream RS arguments can assume cost-threshold bookkeeping without rebuilding it. Imports only Constants and Cost, keeping the dependency surface minimal relative to the forcing chain (T5 J-uniqueness, T6 $\phi$, T7 eight-tick). Used-by edges are empty in the current graph, so the module is a leaf scaffold for later channel-capacity or one-shot coding results rather than a parent of existing theorems. It does not yet connect to the mass ladder, $\alpha$ band, or Berry threshold; those links remain for future Information modules.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)