A Group-Theoretic Approach to Shannon Capacity of Graphs and a Limit Theorem from Lattice Packings

Lean 4 formalization of "A Group-Theoretic Approach to Shannon Capacity of Graphs and a Limit Theorem from Lattice Packings" by Buys, Polak, and Zuiddam.

Definitions

• fractionGraph p q — The fraction graph $E_{p/q}$ on $\mathbb{Z}/p\mathbb{Z}$ where vertices $u, v$ are adjacent iff $\text{dist}(u,v) < q$ (mod $p$). The special case $E_{p/2}$ is the cycle graph $C_p$.
• strongPower G n — The $n$-th strong graph power $G^{\boxtimes n}$
• shannonCapacity G — The Shannon capacity $\Theta(G) = \sup_n \alpha(G^{\boxtimes n})^{1/n}$
• subgroupIndependenceNumber Γ — The subgroup independence number $\alpha_g(\Gamma)$: maximum size of a subgroup that is an independent set
• subgroupShannonCapacity Γ — The subgroup Shannon capacity $\Theta_g(\Gamma) = \sup_n \alpha_g(\Gamma^{\boxtimes n})^{1/n}$

Main Results

Paper	Lean	Statement
Theorem 1.1	limit_cycles	$\lim_{p\to\infty} p/2 - \Theta(C_p) = 0$
Theorem 1.2	limit_fraction_graphs	$\lim_{p/q\to\infty} p/q - \Theta(E_{p/q}) = 0$
Theorem 1.3	subgroup_limit	$\forall \varepsilon > 0$, for $p/q$ large, $\exists a/b = p/q$: $p/q - \Theta_g(E_{a/b}) < \varepsilon$

File Structure

GroupTheoreticShannonCapacity/
├── Main.lean           # Theorem statements (206 lines)
├── MainProofs.lean     # Proofs of main results (1,112 lines)
├── Basic.lean          # Core definitions, upper bound (563 lines)
├── FractionGraphs.lean # Cohomomorphism theory (1,052 lines)
├── Construction.lean   # Parametric construction (2,293 lines)
├── MAlpha.lean         # M_α matrix properties (858 lines)
├── P0Matrix.lean       # P₀ matrix theory (775 lines)
├── Lattice.lean        # Matrix to independent set (708 lines)
└── Defs.lean           # Basic definitions (55 lines)

Dependency Graph

Interactive dependency graph

Main.lean
    │
MainProofs.lean
    │
    ├── Basic.lean ──────────────► Defs.lean
    ├── FractionGraphs.lean ─────► Basic.lean
    ├── Lattice.lean ────────────► Defs.lean
    └── Construction.lean
            │
            ├── MAlpha.lean ─────► P0Matrix.lean
            └── P0Matrix.lean ───► Lattice.lean, Basic.lean

Building

Requires Lean 4 and Mathlib. To build:

lake exe cache get  # Download Mathlib cache
lake build

Acknowledgements

This formalization was developed with the assistance of lean-lsp-mcp.