This roadmap separates completed Lean/site work from active theorem planning, planned theorem work, and later infrastructure milestones. The labels are intentionally conservative: they describe the current repository, not aspirations.
Status Snapshot
| Status | Current meaning | Examples |
|---|---|---|
| Completed | Checked Lean work or completed website/documentation work. | Project B Chunks 1-8, finite Shannon and semantic/KL bridges, stochastic data processing, finite sufficiency, Fano, finite-family, finite convexity, conditional-KL, mutual-independence APIs, and generated reference artifacts. |
| Active | v0.1.x maintenance and downstream adoption. |
The stable baseline contains 31 supported modules, 601 project declarations, and 92 root exports. Provenance, attribution, Apache-2.0 licensing, citation metadata, and versioned API documentation are part of the release contract. |
| Planned | Next technical goals that are not yet formalized or generated. | Later Chapter 2 extensions, theorem-level blueprint work, and optional equation-expanded documentation. |
| Later | Larger infrastructure or research-facing milestones. | Broader finite information theory, downstream applications, and a technical report or paper. |
Completed
- Completed Finite
PMF-based entropy, conditional entropy, mutual information, and conditional mutual information. - Completed Entropy relabeling, zero-entropy characterizations, coordinate reassociation, alphabet/support upper bounds, and uniform-law equality.
- Completed Project B Chunk 1: pair/triple chain rules, support-aware functional dependence, deterministic processing, MI/CMI identities, inequality bands, reviewed aliases, and opt-in units.
- Completed Project B Chunk 2: finite KL support and equality, sharp entropy equality cases, ordinary and conditional independence, and zero-MI/zero-CMI characterizations.
- Completed Project B Chunk 3: finite stochastic channels, Markov characterizations and factorization, MI/KL data processing, invariant-law contraction, and entropy growth under doubly stochastic channels.
- Completed Project B Chunk 4: finite sufficient statistics, exact recovery, common-posterior characterizations, and guarded equality in data processing.
- Completed Project B Chunk 5: deterministic decoding error, exact/q-ary/weak finite Fano inequalities, converse-facing corollaries, examples, API review, generated references, and full milestone validation.
- Completed Project B Chunk 6: dependent finite-family entropy/MI/CMI, ordered chain rules, semantic Shannon inequalities, examples, generated references, full milestone validation, and checkpoint
7b5f0db. - Completed Project B Chunk 7: zero-safe finite log-sum, PMF mixtures, entropy concavity, KL joint convexity and support-aware binary equality, MI input/channel convexity, maintained examples, generated references, independent milestone validation through
C7.22, and checkpoint5e616d8. - Completed Project B Chunk 8: four conditional-family CMI chain rules, common-base conditional KL and joint chain rules, finite-family mutual independence with n-way entropy-additivity equality, maintained examples, generated references, independent milestone validation through
C8.24, and checkpoint1eef228. The required Lean and Pages workflows both pass. - Completed Semantic bridge theorems for expected self-information, conditional laws, KL divergence, fiber formulas, and nonnegativity.
- Completed Release import normalization: lightweight and full mathematical umbrellas, focused semantic declaration ownership, and explicit non-stable anchors.
- Completed Local release trust gates: maintained warning-as-error builds, frozen-API and import-boundary checks, strict source and generated-artifact checks, and project-wide axiom auditing.
- Completed Local package and preliminary legal metadata: toolchain-fixed Lake package metadata, canonical Apache-2.0 licence, CFF citation validation, and exact current source-header audit.
- Completed Release-facing documentation and independently compiled README examples, including tagged dependency, imports, scope, units, limitations, compatibility, and versioned release notes.
- Completed Local Step 11 signature-bearing documentation: 31 supported module pages and all 601 frozen declarations, with optional equation pages omitted and independent final review complete.
- Completed Versioned website staging, navigation, exact-commit source links, upstream-licence inventory, guarded publication workflow, and artifact validation.
- Completed Release checkpoint and plan-health review: the mathematical, units, certificate-boundary, package, API, and trust contracts remain healthy.
- Completed Immutable
v0.1.0GitHub Release, exact-commit Pages publication, Zenodo archival, structured institutional rights-holder metadata, and version DOI10.5281/zenodo.22229599. The tagged CFF remains DOI-free. - Completed Post-release Pages composition: unversioned pages report the current project state, while
/docs/v0.1.0/is rebuilt from and permanently source-linked to the immutable release commit. - Completed Website dashboard, theorem highlights, module guide, source-derived declaration index, module dependency map, and prior-art page.
Next
- Next Maintain source compatibility throughout
0.1.xand respond to downstream adoption feedback. - Planned Evaluate theorem-level leanblueprint pages, a blueprint PDF, and optional equation-expanded API documentation when concrete use justifies their cost.
- Downstream Keep certificate checking, paper-specific constructions, and application automation in separate projects.
Planned
- Planned Extend the current module dependency map toward theorem-level leanblueprint pages and a blueprint PDF; consider optional equation-expanded API documentation only if its cost and use justify it.
- Planned Select any later Cover-Thomas Chapter 2 theorem scope only through a separate readiness and planning process after the Chunk 8 checkpoint.
- Planned Prepare focused mathlib PRs for generic, stable finite-measure lemmas.
Later
- Later Formalize additional reusable finite information-theory results motivated by downstream applications.
- Later Write a technical report or short paper describing the Lean library.