The sphere-covering bound in Lean

We formalize the classical sphere-covering lower bound on the covering number K_q(n,R) in Lean 4, against Mathlib v4.34.1. The library proves that every code over Z/qZ of length n which covers the space at Hamming radius R has at least the ceiling of q^n/V words, where V is the size of a Hamming ball, and it checks eight numerical instances, including K_7(9,4) >= 221. The same archive determines several small covering numbers exactly, among them K_2(7,1) = 16 by the binary Hamming code of length 7, and it exhibits a 12-word covering of (F_2)^6 at radius 1. It does not prove matching upper bounds for the eight instances, does not decide whether those lower bounds improve the literature, and leaves K_2(6,1) >= 11 conditional on a search the kernel did not finish.