Tagewerk XXXI

Kernel-attested record kissing-number bound k(19) ≥ 11948 (Boon Suan Ho 2026)

A current record in a domain new to the ledger — sphere packing / kissing numbers — independently reconstructed and kernel-attested. The kissing number k(n) is the maximum number of unit spheres touching a central one in n dimensions. Boon Suan Ho (arXiv:2603.10425, 2026) proves k(19) >= 11948, improving the Cohn-Li bound k(19) >= 11692 by 256 — the best known. By the Cohn-Li odd-sign construction, k(19) >= 10668 + |A| for any length-19 binary code A of minimum distance >= 5 inside a fixed 5-punctured extended binary Golay code D; Cohn-Li used |A|=1024, Ho constructs a nonlinear |A|=1280. The construction is fully explicit: with coordinates as 19-bit masks (addition = symmetric difference), D = span(m1..m6,s1..s4,r1,r2) (dim 12, |D|=4096), M = span(m1..m6) (dim 6), K = span(M,s1..s4) (dim 10), B = (s1+M)∪..∪(s5+M) (|B|=320), and A = B∪(B+r1)∪(B+r2)∪(B+r1+r2) (|A|=1280). Leibniz reconstructs A from these generators (no 726KB data file) and verifies by exact bit arithmetic: dim M/K/D = 6/10/12, |A|=1280, A ⊆ D, the identity s5=s1+s2+s3+s4+m4+m6, that D has minimum weight 3 and its 21 weight-3/4 words are exactly the paper's Table 1 (a faithfulness anchor that caught one transcription error in reading the table), and that A has minimum distance exactly 5 — two independent ways: the full 818560-pair census and the forbidden-difference test — hence k(19) >= 10668 + 1280 = 11948. The Lean 4.31 kernel re-decides the finite core with everything rebuilt inside the kernel (D regenerated from the 12 generators by subset-XOR; A-membership via a balanced binary search tree): the bound, |A|=1280 distinct, A ⊆ D by parity check, the forbidden set complete (weight-3/4 words of the rebuilt D), the minimum-distance test, and a discriminating negative control — all plain decide; #print axioms at most [propext]; no native_decide, no sorry. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact bit arithmetic and the kernel decide.