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

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) <= 5607 (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. K_7(4,2) = 19 (previously 17 <= K <= 19), and new in this version the equality is entirely checked by the kernel, with no hypothesis (K742.K_7_4_2_eq_19, K742.K_7_4_2_isK): the upper bound is an explicit code; the non-existence of an 18-word code reduces, by lemmas and a code-to-CNF bridge proved in Lean, to 70 SAT instances whose LRAT refutations are replayed inside the kernel by a verified checker (284 modules, 37.8 CPU-hours); the same refutations were checked by two independent checkers outside Lean and confirmed by a second, independent encoding. Also new: a machine-checked ledger of covering-code upper bounds, with formally certified exact entries. Each of the 1145 cells of Kéri's tables carries a certification state and provenance per bound; 486 of the 1145 upper bounds are proved in Lean, in a single theorem, from a generic bound K_q(n,R) <= |C|, construction rules and explicit witnesses. The lower bounds remain citations of the literature, except K_2(6,1) and K_7(4,2), whose exact values are formalized on both sides. Also K_2(6,1) >= 11 by double counting and K_2(6,1) = 12 by a search with a soundness proof.