channel-capacity — Adam Benenson

A Lean 4 library proving that capacity-achieving input priors for Markov kernels are unique under the right non-degeneracy hypothesis. Lean v4.29.1, Mathlib only, warning-free build, zero sorry / admit / axiom.

For the mathematical exposition — why the theorems are shaped the way they are and where the analytic content lives — see docs/overview.md in the repository, or the writing entry on this site.

Three aligned theorems

The library gives three uniqueness theorems that bracket the classical question of when the supremum defining channel capacity is attained at a unique input:

A finite-alphabet theorem that discharges compactness, continuity, and strict concavity internally on Mathlib's canonical weak topology for ProbabilityMeasure. The only external hypothesis is that the kernel's row matrix has trivial real kernel (Kernel.RowMatrixFullRank).
A concrete discharged theorem for compact-Polish channels with a common strictly positive, jointly continuous density against a finite reference measure.
A general measure-theoretic packaging theorem that isolates the abstract hypotheses needed for future upstream generalization, letting callers with their own regularity framework discharge them independently.

The finite theorem is the most immediate Mathlib upstream candidate; the discharged theorem is the strongest concrete measure-theoretic result in the repository; the general theorem is the abstract packaging both specialize.

Counterexample

The library includes a Fin 6 → Fin 3 permutation-channel counterexample showing that pairwise distinctness of rows (RowSeparating) is strictly weaker than the injectivity of the prior pushforward map that the uniqueness theorems actually need. Two distinct input priors can push forward to the same output marginal; the non-degeneracy hypothesis cannot be relaxed to mere row separation.

Role in the legitimacy thread

The motivating application is a Shannon-correspondence for governance channels in the legitimacy framework; that development consumes this library as a dependency and is documented in its own paper. The present library stands on its own information-theoretic terms.