{"id":"palomar/PALOMAR-2026-10-21-000003","url":"https://github.com/jtraverso/lovasz-theta/tree/2d506b5abca378d9133b5e3f1264a5316843c9a7","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000003-v1.json","repo":"https://github.com/jtraverso/lovasz-theta","tags":["math.CO","cs.IT","msc:05C69","msc:94A15","msc:05C50","graph-theory","shannon-capacity","independence-number","lean-formalization"],"score":0,"title":"Lovász's bound on the Shannon capacity","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Lovász's orthonormal-representation bound on the independence number (if u is an orthonormal representation of G with handle c and 1 ≤ t (c·u_i)² for every vertex, then α(G) ≤ t), of its multiplicativity under strong powers (α(G^⊠k) ≤ t^k), and of its application to the pentagon: α(C₅^⊠k)² ≤ 5^k for every k, Shannon's α(C₅^⊠2) = 5, and hence the Shannon capacity Θ(C₅) = √5. Mathlib has independence numbers but neither strong graph products nor the Shannon capacity.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"On the Shannon capacity of a graph","identifier":"doi:10.1109/TIT.1979.1055985","relationship":"formalizes"},{"title":"The zero error capacity of a noisy channel","identifier":"doi:10.1109/TIT.1956.1056798","relationship":"formalizes"}]}