Channel and question
- Input
- \(X\in\mathcal X\)
- Output
- Legitimate output \(Y\) and eavesdropper output \(Z\).
- Law
- The channel is memoryless and physically degraded: \(X\to Y\to Z\).
- Quantity
- Secrecy capacity \(C_s\), measured in secret bits per channel use.
Criterion. Reliable communication with asymptotically vanishing leakage.
- Reliability is required at Y.
- Information leakage to Z vanishes under the stated secrecy criterion.
Current status
\[C_s=\max_{P_X}\bigl[I(X;Y)-I(X;Z)\bigr]\]
Conditions. The channel is physically degraded.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_s\ge\max_{P_X}[I(X;Y)-I(X;Z)]\) | Stochastic encoding and random binning. | 1975 |
| Upper | \(C_s\le\max_{P_X}[I(X;Y)-I(X;Z)]\) | Fano's inequality, secrecy, and degradedness. | 1975 |
Formal verification
Lean coverageFormally stated
Concrete operational definitions and admitted research statements are present. Existing proofs are preserved. New statements require mathematical review and proof completion.
Claims
- The degraded finite wiretap formula with unnormalized leakage tending to zero.
operational-capacity· exact capacity · solved · Formally stated · v1
Lean declarations (1)
CapacityAtlas.Claims.degradedWiretapclaim · operational-capacity
lean/CapacityAtlas/Claims/DegradedWiretap.lean — The degraded finite wiretap formula with unnormalized leakage tending to zero.
References
- Aaron D. Wyner (1975). The Wire-Tap Channel. Bell System Technical Journal. DOI 10.1002/j.1538-7305.1975.tb02040.x.
- Abbas El Gamal and Young-Han Kim (2011). Network Information Theory. Cambridge University Press. DOI 10.1017/CBO9781139030687.