covering-codes

Lean 4 formalization of q-ary covering codes with a proof-carrying database of certified bounds for K_q(n,r)

Lean 4-verified lower bound for binary twofold covering codes: K(8,1,2) >= 61, plus an elementary even-n theorem improving five published bounds. First unknown term of OEIS A004045.

Certified proof frontier for K_3(6,2): exact dual certificates exclude six of 38 normalized branches; the global interval is unchanged.

GPU framework for covering-type combinatorial search: covering codes, dominating sets, multiple coverings

Certified scoped theorem for binary covering sequences: every valid length-70 (9,1) cover uses at most 60 distinct edges in common with one fixed backbone; global bounds unchanged.

Certified scoped theorem for K_3(7,3): eight seven-word subcores are excluded from all size-at-most-11 covers; the global interval is unchanged.

Certified proof frontier for K_2(11,3): 112/150 normalized and 324/350 selected branch closures; the exact value remains open.