Tagewerk XXV

Kernel-attested cap-set subgroups of finite fields (SET, EvenQuads, and the GF(2^2n) family; Kable–Mills–Wright 2026)

A fresh 2026 result in a domain new to the ledger — additive combinatorics over finite fields / cap sets — independently confirmed and kernel-decided. A cap set contains no full line of its affine geometry: in AG(k,3), the card game SET, a line is three distinct points summing to 0; in AG(k,2), the game EvenQuads, a 'quad' is four distinct points summing to 0. Kable, Mills & Wright (arXiv:2604.26989) show certain MULTIPLICATIVE subgroups of a finite field, seen inside the field's ADDITIVE geometry, are cap sets. Leibniz re-decides these from the field axioms, using none of the paper's tables: it builds GF(pᵏ) = F_p[t]/(irreducible), confirms it is a genuine field (multiplicative group cyclic of order pᵏ−1), forms the power-subgroup, and checks the cap property by exact finite-field arithmetic over every triple (char 3) or quad (char 2). It confirms: the 20 nonzero fourth powers of GF(81) are a SET-cap (no 3 sum to 0 in AG(4,3)); the 9 nonzero seventh powers of GF(64) are an EvenQuads-cap (no 4 sum to 0 in AG(6,2)); and the general theorem that the (2ⁿ−1)-th powers form a cap of size 2ⁿ+1 in GF(2^{2n}), verified for n=2..5 (sizes 5, 9, 17, 33). Both marquee subgroups are the MAXIMAL caps for their decks (sizes 20 and 9), an external cross-check; and the cap property is model-independent — Leibniz re-verifies GF(81) with a second irreducible polynomial and obtains the same 20-cap. The Lean 4.31 kernel then independently decides the two marquee caps over the explicit (F₃)⁴ / (F₂)⁶ element vectors (plain decide, #print axioms = propext only; no native_decide, no sorry). Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact finite-field arithmetic and the kernel decide.