Binary twofold covering codes: K(8,1,2) ≥ 61, verified in Lean 4

A machine-checked lower bound for multiple covering codes, and an elementary theorem for all even n that improves the published lower bound at five tabulated positions.

Abstract

A binary code C ⊆ F₂ⁿ is a twofold covering of radius 1 if every point of F₂ⁿ lies within Hamming distance 1 of at least two codewords; K(n,1,2) denotes the least size of such a code. We prove that for even n

|C| ≥ ⌈ 3·2^(n+1) / (3n+2) ⌉

by a half-page parity refinement of the covering-excess method of Johnson and van Wee. The bound strictly improves the best published lower bound for every even n ≥ 6, and gives the exact value K(6,1,2) = 20 with no computer search, where the published value came from integer programming.

The case n = 8 is the first unknown term of OEIS A004045, where the published record was 59 ≤ K(8,1,2) ≤ 64. A second, computational argument refutes |C| = 60, and that argument is formalised in Lean 4 with zero sorrys.

The five published lower bounds this improves

Published lower bounds are those of Krotov and Potapov (2021). The ratio to the old bound tends to 1, but the additive gap grows like (2/3)·2ⁿ/n² and is unbounded, so the improvement does not run out.

The formal statement

le_card_of_isDoubleCover : ∀ (C : Finset V), IsDoubleCover C → 61 ≤ C.card
  depends on axioms: [propext, Classical.choice, Quot.sound]

No sorryAx and no native_decide. The trusted base is Lean's kernel plus the four definitions the statement mentions transitively — V, dist, cov, IsDoubleCover — which the author has read. Every declaration's axiom trace is printed by lake build Mcov.Audit.

What is not established

• The upper bound is untouched and remains 64. That bound is older than usually credited: it is already the doubling K(8,1,2) ≤ 2·K(7,1,2) = 64 in the 1993 table of Hämäläinen, Honkala, Kaikkonen and Litsyn. Östergård's 1995 tabu-search paper improves 27 upper bounds in that table, but n = 8, μ = 2 is not among them.
• Novelty is not claimed for the method. Krotov and Potapov already apply Delsarte nonnegativity to a covering code's own distance distribution, and a Chen–Li manuscript cited in the literature could not be located.
• A prescribed-automorphism result — that every twofold covering with at most 63 codewords is asymmetric — rests on a weaker footing: 4 of 28 classes are machine-certified, the other 24 are floating-point solver verdicts.
• No human has reviewed the proofs, which rest on Lean's kernel, and the work has had no peer review. Generative AI was used extensively; see the Declarations section of the paper.

Reproducing it

git clone https://github.com/SeverinVisionary/oeis-a004045
cd oeis-a004045 && ./reproduce.sh

Twelve self-asserting checks, about a minute, Python standard library only apart from one step needing SciPy for small LP control cases; non-zero exit on any failure. The Lean development is a separate build of about four minutes.

Read further

• The paper — full statements, proofs and references
• The paper as a PDF — a typeset rendering of PAPER.md, unchanged in content; its first page names the commit it was rendered from
• Plain-language note — what this is, for non-specialists
• Prior art — what was already known, and the open priority question
• Zenodo archive — versioned, with the exact-rational certificates