Covering codes checked by the Lean kernel: K_7(9,4) <= 1134, ten more upper bounds, and K_2(6,1) = 12

Lean 4 proofs, against Mathlib v4.34.1 and checked by the kernel with no sorry and no native_decide, of upper bounds on the covering number K_q(n,R) for eleven cells, each by an explicit code below the corresponding table entry we found: K_7(9,4) <= 1134 (best published 1475, Marosi, arXiv:2608.19872v3), K_7(10,4) <= 5616 (previously 6517), K_5(11,4) <= 2875 (previously 3125) and K_5(10,5) <= 162 (previously 175), three cells unchanged in Kéri's tables since at least 2004, and K_7(8,3) <= 1887, K_5(10,4) <= 625, K_5(9,3) <= 1250, K_5(7,2) <= 500, K_5(9,4) <= 250, K_4(10,4) <= 192, K_5(9,5) <= 50. Two certificates: digit prefixes (12 CPU-hours for (Z/7)^9) and syndromes of a linear base (minutes; the 5616-word code in 11 minutes on four cores), each new certificate also tested by mutations that the kernel rejects. All codes are cosets of a linear code plus a patch; for K_7(9,4) the base comes from an enumeration of all 6362 classes of non-degenerate [9,3]_7 codes, and the 105-word patch is optimal among patches invariant under translation along either of the two lines of the base solved to optimality by integer programming. A literature search over 2103 works found no smaller published code in the four cells. Also K_2(6,1) >= 11 by double counting and K_2(6,1) = 12 by a search with a soundness proof.