Lean 4 kernel check of three Green-Tao colourings of the N smallest primes

Lean 4 kernel checks (decide +kernel, no native_decide, Lean core only) of three colourings of the N smallest primes published by D. Bentley (github.com/DuncanBentley/green-tao-bounds, tag v0.2.0, commit a090c3b7; Zenodo 10.5281/zenodo.23854101): 4 colours with pattern 3-3-3-4 for N = 1063, 4 colours with 3-3-4-4 for N = 3013, and 3 colours with 4-4-5 for N = 16953. The colourings and the bounds they give are Bentley's; this upload checks them and states no bound of its own. Each theorem states that the list is exactly the N smallest primes (primality by trial division, proved sound in Lean; every other number in [2, p_N] has a factor witness), that the colour bit masks are pairwise disjoint and their union is the list's mask, and that colour i has no l_i-term arithmetic progression of prime values. The colouring then witnesses grt_k(l_1, ..., l_k) > N in the sense of O. Kullmann (arXiv:1004.0653, Def. 13). There is no Lean definition of grt. Axioms: [propext, Classical.choice, Quot.sound]. The colouring files are MIT-licensed (Copyright (c) 2026 Duncan Bentley) and are included unchanged with their licence text.