Capacity Atlas Channel-capacity problems
Community maintained

Contribute to Capacity Atlas

Use a pull request for canonical data or Lean code. Use an issue to discuss uncertain claims before editing.

Open an issueFork the repository
01 · Problems

Add a capacity problem

Copy an existing file in data/problems. A problem is not merely a channel name. It fixes the information pattern, constraints, error criterion, and requested quantity.

  1. Choose a stable lowercase identifier and matching YAML filename.
  2. Specify the channel model so a reader can reconstruct the problem without opening a paper.
  3. Record the current result as an exact formula, characterization, region, or explicit lower and upper bounds.
  4. Add primary references to data/references.yaml.
  5. For an open entry, explain the bottleneck and concrete forms of progress.
Scope rule. Separate variants when feedback, state knowledge, zero-error criteria, cost constraints, code linearity, or another assumption changes the capacity question.
02 · Bounds

Update a bound

Bounds are first-class records. Do not replace a number without preserving its provenance and conditions.

bounds:
  - id: descriptive-bound-id
    direction: lower
    relation: 'C \ge R'
    method: One-sentence description of the code or converse.
    year: 2026
    conditions: Optional parameter range.
    references: [paper-id]

For numerical or computer-assisted results, link the paper and note the certificate or implementation in the method or notes field. The initial release does not display non-Lean proof-assistant artifacts as formal proofs.

03 · Lean

Add a Lean formalization

Reuse the definitions in lean/CapacityAtlas. Add a shared abstraction only when at least two entries can plausibly use it.

  1. Add the Lean file and import it from lean/CapacityAtlas.lean.
  2. Prove all stochasticity and well-formedness obligations.
  3. Use no sorry, admit, or hidden axiom.
  4. List every displayed declaration in the problem YAML.
  5. Set the status conservatively: definitions, statement, partial, or complete.

A complete badge means the capacity claim shown on the page is proved. A valid channel definition alone earns the definitions badge, not a proof badge.

04 · Checks

Run the same checks as CI

python -m pip install -e '.[dev]'
make check
cd lean
lake build

make check validates the schema, reference identifiers, Lean file links, named declarations, Python tests, formatting, and a complete static-site build.

05 · Review

What maintainers review

  • The model and rate convention are unambiguous.
  • Every factual claim has a primary source.
  • The displayed bounds are current and carry their parameter ranges.
  • Open-problem language distinguishes conjecture from theorem.
  • Formalization status matches what Lean actually checks.
  • The contribution stays small enough to maintain.