Channel and question
- Input
- At use i the encoder chooses a symbol from a finite nonempty alphabet as a deterministic function of the message and outputs strictly before i.
- Output
- A symbol from a finite nonempty alphabet is observed by the decoder and fed back noiselessly before the next use.
- Law
- Conditional on the message and past outputs, the next output has the fixed transition law \(W(y_i\mid x_i)\).
- Quantity
- Feedback capacity \(C_{\mathrm{fb}}(W)\), measured in bits per channel use.
Criterion. The supremum of rates supported at every sufficiently large fixed blocklength with vanishing average error and strictly causal output feedback.
- Feedback is noiseless, strictly causal, and unlimited; both terminals know the forward channel law.
- Blocklengths are fixed in advance, with no variable stopping time.
- Messages are uniform, encoders and decoders are deterministic, and average decoding error vanishes.
- There is no input-cost constraint.
Current status
\[C_{\mathrm{fb}}(W)=C(W)=\max_{P_X}I(X;Y)\]
Shannon's Theorem 6 proves the ordinary feedback-capacity equality; Theorem 7 concerns the separate zero-error problem. The feedback model and theorem are verified in the Collected Papers reprint, pages 232–234. The formal direct proof inherits the all-sufficiently-large-blocklength guarantee from the ordinary DMC coding theorem.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_{\mathrm{fb}}\ge C\) | Embed ordinary DMC codes by choosing the same input word regardless of feedback, preserving rate and error exactly. | 1956 |
| Upper | \(C_{\mathrm{fb}}\le\max_{P_X}I(X;Y)\) | Each adaptive channel use contributes at most the single-use mutual-information maximum; sum over the block and apply Fano's inequality. | 1956 |
Formal verification
Lean coverageFormally stated
The local proof embeds ordinary codes with the same rate and error. The converse uses a sequential entropy bound and Fano’s inequality.
Claims
- Fixed-blocklength average-error capacity with arbitrary strictly causal noiseless feedback policies equals the ordinary finite-DMC mutual-information maximum.
exact-capacity· exact capacity · solved · Formally proved · v1
Lean declarations (5)
CapacityAtlas.Feedback.PolicyAPI
lean/CapacityAtlasForMathlib/InformationTheory/Feedback.lean — Inputs depend on the message-specific policy and outputs strictly before the current use.CapacityAtlas.Feedback.blockChannelAPI
lean/CapacityAtlasForMathlib/InformationTheory/Feedback.lean — Normalized physical output law of each adaptive feedback policy.CapacityAtlas.Feedback.BlockCodeAPI
lean/CapacityAtlasForMathlib/InformationTheory/Feedback.lean — Deterministic fixed-length feedback code with a positive message count.CapacityAtlas.Feedback.operationalCapacityBitsAPI
lean/CapacityAtlasForMathlib/InformationTheory/Feedback.lean — Average-error capacity over all sufficiently large fixed blocklengths.CapacityAtlas.Channel.feedbackCapacityStatementclaim · exact-capacity
lean/CapacityAtlas/Channels/Feedback.lean — Canonical ordinary feedback-capacity proposition.
Linked proofs (1)
- exact-capacity · complete · claim v1
TomasOrtega/CapacityAtlasFeedback@b35299f2·CapacityAtlasFeedback.capacityCertificate
Historical upstream certificate imported into this repository. Pins Atlas commit c0d665982bab3c4840bac511e950cdf3fc48b50c. The upstream audit checks transitive proof axioms and full canonical-proposition correspondence with rigid universes; negative controls reject a different proposition and a universe-restricted certificate.
References
- Claude E. Shannon (1956). The Zero Error Capacity of a Noisy Channel. IRE Transactions on Information Theory. DOI 10.1109/TIT.1956.1056798.
- Thomas M. Cover and Joy A. Thomas (2006). Elements of Information Theory. Wiley, second edition. DOI 10.1002/047174882X.