A Lean 4 formalisation of lower bounds on the Shannon capacity of the odd cycles
C₇, C₁₁, C₁₃, C₁₅, C₁₉, C₂₁, C₂₃.
Pjotr Buys (Centrum Wiskunde & Informatica), Sven Polak (Tilburg University), Jeroen Zuiddam (University of Amsterdam).
Paper: arXiv:2607.29681, which will be updated to match. The bounds proved here are stronger than those in its first version; see the paper for the method and for context.
Our results build on methods of Gao (arXiv:2607.27869) and of Itty, Rosin, Carstensen and Reichman (arXiv:2607.21517).
The independent sets used as the basis of the constructions are due to Baumert, McEliece, Rodemich, Rumsey, Stanley and Taylor (1971); Codenotti, Gerace and Resta (2003); Polak and Schrijver (arXiv:1808.07438); and De Boer, Buys and Zuiddam (arXiv:2404.16763). See the paper for more details.
We obtain the following bounds, formally stated in ShannonBounds/Main.lean.
| n | Θ(Cₙ) ≥ | p | digits |
|---|---|---|---|
| 7 | 3.258827985920007 | 500 | 257 |
| 11 | 5.295492315784620 | 207 | 150 |
| 13 | 6.302926729310108 | 522 | 418 |
| 15 | 7.301628695930103 | 3664 | 3164 |
| 19 | 9.357200030000796 | 11856 | 11514 |
| 21 | 10.347918137743866 | 4 | 5 |
| 23 | 11.334557922754518 | 3040 | 3206 |
Each row comes from an independent set of size N in Cₙ^⊠p, so Θ(Cₙ) ≥ N^(1/p); the
digits column is the number of decimal digits of N. The decimals are truncated rather
than rounded, so each is a genuine lower bound.
Every bound is proved from Mathlib with no sorry; the certificates are checked by
native_decide.
ShannonBounds/Main.lean |
the capacity bounds |
ShannonBounds/Defs.lean |
Shannon capacity, strong product and strong power |
ShannonBounds/BaseC{n}*.lean |
the base independent sets and the construction built from them |
ShannonBounds/CycleC{n}.lean, CapC{n}.lean |
identify the graph used in the data files with a strong power of cycleGraph n |
ShannonBounds/CosetC21.lean |
the C21 union-of-cosets code, and the C21 bound |
ShannonBounds/CosetC23*.lean |
the C23 code and the port system it carries |
ShannonBounds/Layered.lean, Lift.lean, Flatten.lean, PortRealisation.lean, Reindex.lean |
the framework the certificates are expressed in |
ShannonBounds/Substitutions.lean, TerminalCodes.lean |
the substitution tables and terminal codes the certificates are built from |
ShannonBounds/CertC{n}.lean, CapCertC{n}.lean |
the certificates in the table above, and their capacity statements (n != 21) |
ShannonBounds/Decimal.lean |
from an exact root to the truncated decimal |
Lean 4.32.2 and the matching Mathlib, both pinned in lean-toolchain and lakefile.toml.
lake exe cache get
lake build
lake build ShannonBounds.Main builds the bounds and everything they depend on.
After lake exe cache get, a clean build takes about three minutes on 32 cores. At most
eleven Lean processes run at once, together peaking at about 13 GB of memory, so a machine
with fewer cores needs proportionally longer but no more memory.
| 2026-08-02 23:40:22 +0200 | first release |
| 2026-08-10 11:10:00 +0200 | update of bounds |