Three-sunflower-free set systems with bounded pairwise intersections

Version 2 (June 2026): the t=1 extremal classification is now fully kernel-verified in Lean 4 (companion release paper-v2, doi:10.5281/zenodo.20693191), and a structural reduction at t=2 is added. The t=1 value and t=2 bracket are unchanged from version 1. Paper and deterministic verification artifacts for the extremal function M(l,t): the largest 3-sunflower-free family of l-element sets with pairwise intersections of size at most t. Exact determination M(l,1) = 2l+2 with extremal classification; M(l,2) = Theta(l^2) with upper bound 3l^2-l+2 via a counting argument and lower bound via doubled pencil families of orthogoval projective planes (CIJSSS, arXiv:2210.11961); certified small exact values. The archive contains the paper (PDF + TeX source), the deterministic checker scripts (.mjs, Node.js, dependency-free) with their JSON output certificates, and pointers to the Lean 4 formalization (kernel-verified structural spine; SAT/LRAT and explicit-witness lanes via native finite reduction) at https://github.com/SproutSeeds/sunflower-lean, release paper-v1, archived at doi:10.5281/zenodo.20670535 (see FORMAL_RESULTS_M3.md there for the paper-to-Lean mapping).