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; 700 of the 1145 upper bounds are theorems of the Lean kernel, almost all 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. New in version 0.9.0: three exact values that are potentially new (not found in the literature we searched), whose lower bounds are verified computational certificates checked by exact programs outside Lean, not theorems of the kernel. K_3(6,2) = 17 (previously 15 <= K <= 17; Bertolo-Östergård-Weakley 2004, doi:10.1002/jcd.20008, and Hämäläinen-Rankinen 1991, doi:10.1016/0097-3165(91)90024-B): after a normalization by a minimal fibre, codes with 15 or 16 words fall into 12049 and 12674 instances whose linear relaxations are infeasible by 12054 and 13099 integer Farkas certificates checked in exact arithmetic, independently reproduced by a second pipeline with no code in common (VeriPB and LRAT proofs); the upper bound 17 is a kernel theorem in the ledger. K_7(6,4) = 14 (previously 13 <= K <= 15; Haas-Schlage-Puchta-Quistorff 2009, Kéri-Östergård 2005): a new 14-word code, formalized in Lean, and LRAT refutations of the 8008 fibre profiles of a 13-word code, from a fibre lemma for K_q(n,n-2). K_7(5,3) = 17 (previously 15 <= K <= 17, both announced in Kéri's tables): LRAT refutations of one profile for 15 words and of all 201376 profiles for 16 words; the upper bound 17 was the announced one, with no published code. New in version 0.9.1: a 17-word code of our own for K_7(5,3), whose covering property is a theorem of the Lean kernel (CoveringK753.K_7_5_3_le_17, axioms propext, Classical.choice and Quot.sound only), so both bounds of K_7(5,3) = 17 are now established here, the upper one in the kernel and the lower one as verified computational certificates. Each lower bound survived an adversarial review; the remaining gaps (for example, 9 large LRAT proofs of K_7(5,3) not regenerated by the review, and no Lean proof of the three lower bounds) are stated in the paper, together with the limits of the same methods on other open cells. New in version 0.10.0: K_4(7,4) ≥ 10 and K_4(6,3) ≥ 12 (previously 9 and 11), by LRAT refutations of all 792 and 8008 fibre profiles, from the fibre lemma extended to every radius up to n-2, checked by lrat-check and again by a second solver on every profile and by an independent encoding on a sample; these are verified computational certificates outside Lean, new in the ledger; we did not find them in the sources we read, but novelty is not established (one source, Haas 2011, Ars Combin. 99, not read), and an independent adversarial review is pending. With a 10-word code of our own checked by the official verifier, K_4(7,4) = 10. The certified upper bounds rise to the count stated above (bases outside the batch generator and 26 linear codes found by search), all equal to published values. Negative results recorded: tabu search with and without prescribed groups ties four records and beats none, and construction programs evolved by a language model lost to plain local search. The paper adds the method (witness, independent verifier, kernel, objective bound), the infrastructure with a budget enforced in code, and related work on mathematics with AI in 2026; every ledger count in the paper is generated from the ledger by a script.