A formally verified three-point bound: a kissing configuration in dimension five with at least 43 points has at most five antipodal pairs

A kissing configuration in R^5 is a set of unit vectors with pairwise inner products at most 1/2; an antipodal pair is a pair {x, −x} of its points. Every kissing configuration in R^5 with at least 6 antipodal pairs has at most 42 points; equivalently, a kissing configuration with at least 43 points has at most 5 antipodal pairs. The theorem and its certificate (an exact rational certificate at degree 12 for a Bachoc–Vallentin three-point bound in which the points carry two types, paired and unpaired) were made public in an earlier preprint, doi:10.5281/zenodo.24194413. This paper gives a formal proof of the theorem in Lean 4 with Mathlib. The final Lean theorem (PC.paircap5R) has no hypotheses and depends only on the three standard axioms propext, Classical.choice and Quot.sound. No output of compiled code is trusted (no native_decide). The formal proof includes the positivity of the Bachoc–Vallentin and Schoenberg kernels on S^4 up to degree 12, the typed counting argument, verified checkers (positive definiteness by exact elimination; positivity on the Gram-feasible part of a box by Bernstein subdivision with a multiplier for the Gram determinant), and 6421 box checks evaluated by the Lean kernel. The proof of kernel positivity is adapted from the Lean development of alejandrozarco (doi:10.5281/zenodo.24145124, Apache-2.0) and extended from degree 8 to degree 12. The supplement contains the complete Lean project, rebuild instructions, the logs, and a file that traces every number in the paper to a log line. This does not change the known bounds on τ5: τ5 ≥ 40, the best published upper bound is τ5 ≤ 44 (Mittelmann and Vallentin 2010), and a 2026 preprint by T. S. Tomar (doi:10.5281/zenodo.24093811) gives τ5 ≤ 43 with an exact computer certificate (not yet refereed; not used here). We claim no priority on τ5 ≤ 43. The result concerns exact antipodal pairs only, and the method does not exclude 5 pairs. Limits: the build was done in several sessions and one build from scratch was not timed; the proof objects were not re-checked with an independent external checker; the lower-degree certificates for seven pairs and the floating-point remarks are not formalized. AI use: the derivations, the certificate, the checkers, the Lean formalization and the text were produced with Claude (Anthropic) under the author's direction. The theorem rests on the Lean kernel accepting the proof, not on the AI system. Not yet peer reviewed. Contact: gameruchral71@gmail.com.