Channel and question
- Input
- A binary symbol inserted into a box already containing one binary state symbol.
- Output
- One of the two symbols is selected uniformly as output; the other becomes the next state.
- Law
- The same trapdoor state transition as the feedback entry, but the encoder observes no channel outputs.
- Quantity
- Feedforward capacity \(C\), measured in bits per channel use.
Criterion. Nonfeedback encoding over arbitrary blocklengths.
- The initial state is fixed and known.
- Average decoding error vanishes.
Current status
\[0\le C\le1\]
The exact value is not identified with the solved feedback capacity.
| Result | Relation | Method | Year |
|---|---|---|---|
| Upper | \(C\le1\) | Binary input alphabet bound. | 2006 |
| Lower | \(C\ge0\) | One-message code. | 2006 |
Research frontier
Determine the exact capacity without encoder access to past outputs.
Why it remains open. Channel state depends on the unobserved output history and creates input-dependent memory.
What would count as progress
- Improve finite-state achievability and converse bounds under a fixed initial-state convention.
Concrete tasks
- doneKeep the solved feedback capacity as a separate operational statement.
Lean formalization
Canonical statementStatement
Version 1 · Lean. A separate feedforward operational interface prevents accidental reuse of the feedback theorem.
CapacityAtlas.Channel.trapdoorWithoutFeedbackCapacityBoundsstatement
lean/CapacityAtlas/Channels/Trapdoor.lean — Basic feedforward-capacity bounds for the fixed trapdoor transition.
Substantial proofs0 linked
No external Lean proof is registered. Proofs longer than roughly 50 lines or requiring problem-specific infrastructure should live in a dedicated repository and link back to this statement version.
References
- Haim H. Permuter, Paul Cuff, Benjamin Van Roy, and Tsachy Weissman (2006). Capacity of the Trapdoor Channel with Feedback. arXiv preprint.
Discussion
Thread key: capacityatlas:trapdoor-channel-without-feedback