Channel and question
- Input
- \(X\in\mathbb R\) with average power \(P\).
- Output
- \(Y=X+N_1\) and \(Z=X+N_2\).
- Law
- Gaussian noise variances satisfy \(\sigma_1^2<\sigma_2^2\).
- Quantity
- Secrecy capacity \(C_s\), measured in secret bits per channel use.
Criterion. Strong-secrecy capacity with the per-message-and-seed block-power constraint stated above.
- The eavesdropper channel is degraded.
- For every message m and every private seed s, sum_t x_t(m,s)^2 <= n P. This constraint is not averaged over the message or the seed.
- The finite private seed is uniform and independent of the uniform message.
- Strong secrecy means unnormalized I(M;Z^n) tends to zero, simultaneously with legitimate average decoding error.
Current status
\[C_s=\frac12\log_2\!\left(1+\frac{P}{\sigma_1^2}\right)-\frac12\log_2\!\left(1+\frac{P}{\sigma_2^2}\right)\]
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_s\ge C(\sigma_1^2)-C(\sigma_2^2)\) | Gaussian stochastic encoding and binning. | 1978 |
| Upper | \(C_s\le C(\sigma_1^2)-C(\sigma_2^2)\) | Degraded secrecy converse and Gaussian extremality. | 1978 |
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. Power convention: MessageSeedPowerAdmissible. No equivalence to another power convention is assumed.
Claims
- Degraded Gaussian strong-secrecy capacity with private finite randomization.
operational-capacity· exact capacity · solved · Formally stated · v1
Lean declarations (1)
CapacityAtlas.Claims.gaussianWiretapclaim · operational-capacity
lean/CapacityAtlas/Claims/GaussianWiretap.lean — Degraded Gaussian strong-secrecy capacity with private finite randomization.
References
- S. K. Leung-Yan-Cheong and Martin E. Hellman (1978). The Gaussian Wire-Tap Channel. IEEE Transactions on Information Theory. DOI 10.1109/TIT.1978.1055917.