Certified SAT artifacts for Frankl's union-closed sets conjecture under transitive group symmetry on 14 points (DRAT certificates for the five minimal instances)

v1.1.0 (15 Aug 2026): degree 15 closed. This version adds the three degree-15 certificates; the description below covers the complete dataset. Heavy computational artifacts supporting the repository frankl-transitive-sat: computer-assisted proofs that no non-trivial union-closed family on 14 or 15 points invariant under any transitive permutation group violates Frankl's union-closed sets conjecture. Together with the predecessor's cyclic results (doi:10.5281/zenodo.21900942) and the degree-13 Cauchy corollary, the transitive case of the conjecture is closed up to 15 points. Degree 14. Via an invariance-descent lemma and a reduction to minimal transitive groups (census: 63 transitive groups of degree 14, of which 26 contain no 14-cycle), the theorem reduces to the already-certified cyclic case Z14 (doi:10.5281/zenodo.21900943) plus five group instances: 14T2 (regular D7), 14T6 ([2^3]7), 14T10 (L7(14)), 14T12 (1/2[D(7)^2]2) and 14T30 (PSL(2,13)). Each is UNSAT for family size ≥ 3 (sizes ≤ 2 conform trivially, Sarvate–Renaud reduction), decided by two independent exact methods — OR-Tools CP-SAT and CaDiCaL on an independently written encoding — with DRAT certificates verified by drat-trim (s VERIFIED on all five). Degree 15. Census from GAP's transitive-groups library: 104 groups, of which 78 contain a 15-cycle and reduce to the certified cyclic case Z15 (LRAT certificate archived at doi:10.5281/zenodo.21939129); the 26 without reduce, by minimality lemmas, to three instances — 15T5 (A5, 686 orbit variables), 15T9 ([5^2]3, 478) and 15T26 ([3^4]5, 222) — each decided UNSAT by CP-SAT + CaDiCaL with LRAT certificates verified by lrat-check and re-verified by the formally verified checker cake_lpr. Files (xz-compressed): for each G in {14T2, 14T6, 14T10, 14T12, 14T30}: G.cnf.xz (DIMACS instance, deterministic output of dump_dimacs_group.py G 3) and G.drat.xz (verified DRAT certificate; 14T2.drat is 3.3 GB decompressed) — hashes in SHA256SUMS-certificates.txt. For each G in {15T5, 15T9, 15T26}: G.cnf.xz and G.lrat.xz (verified LRAT certificate) — hashes in SHA256-15T-cnf.txt, SHA256-15T-lrat.txt and SHA256-15T-xz.txt. Plus DEGREE15-CLOSED.md, the degree-15 theorem record with re-verification commands. Verification recipes. Degree 14: unxz a pair, check hashes, run drat-trim G.cnf G.drat; expect s VERIFIED (14T30/14T12/14T10 in under a second, 14T6 ~4 s, 14T2 ~50 minutes, <2 GB RAM). Degree 15: unxz a pair, check hashes, run lrat-check G.cnf G.lrat; expect the line c VERIFIED (all three in seconds) — never trust exit codes alone. Full mathematical statements, the census and minimality scans, measured resource data and reproduction instructions: see the repository's README.md, docs/theorem-degree14.md, docs/theorem-degree15.md, results/FOUND.md and results/DEGREE15-CLOSED.md. The computations were carried out with Anthropic's Claude Code (model claude-fable-5, no fallback) — the degree-14 campaign by an autonomous agent loop, the degree-15 closure in interactive sessions — under human supervision, on one 16 GB laptop and a consumer Claude subscription (Max 20×).