Shannon capacity of the pentagon

shannon_capacity_pentagon — a formalization challenge from the lean-eval benchmark.

Notes

Lovász's computation: the Shannon capacity of the five-cycle C₅ is √5. The helpers IsIndependent, independenceNumber, strongPower, and HasShannonCapacity encode the capacity as the limit of (α(Gᵏ))^{1/k}, modelling length-k words as Fin k → V. Mathlib has finite simple graphs and cycle graphs but no Shannon capacity, strong graph powers, Lovász theta number, or the semidefinite-programming bound. Category-(b) candidate.

Formal statement

/-- **Lovász's theorem on Shannon capacity of the pentagon** (§238).
The Shannon capacity of the five-cycle is `√5`. -/
theorem shannon_capacity_pentagon :
    HasShannonCapacity (SimpleGraph.cycleGraph 5) (Real.sqrt 5) := by
  sorry

Informal solution sketch

Lovász's theta-function argument. Lower bound: the strong square C₅⊠C₅ has an independent set of size 5 (e.g. {(0,0),(1,2),(2,4),(3,1),(4,3)}), so α(C₅⊠C₅) ≥ 5, giving capacity ≥ √5. Upper bound: the Lovász number ϑ is multiplicative under the strong product and satisfies α(G) ≤ ϑ(G), so the capacity Θ(G) = lim (α(Gᵏ))^{1/k} ≤ ϑ(G); computing ϑ(C₅) = √5 (via the umbrella/orthonormal-representation construction, or the eigenvalue bound for vertex-transitive graphs) gives capacity ≤ √5. The two bounds coincide at √5.

Source

Knill, Some fundamental theorems in mathematics, §238.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: shannon_capacity_pentagon
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.