A Lean-Verified Counterexample to Graffiti3 Conjectures 21 and 22

This preprint gives a finite 2-group refuting Conjectures 21 and 22 in Appendix C of Randy Davila's Graffiti3 preprint. The group is the semidirect product of the additive group of F_2[t]/(t^7) by C_8, with a cyclic generator acting by multiplication by 1+t. It has order 1024, derived-subgroup order 64, abelianization order 16, exponent 8 and 40 conjugacy classes. The two proposed lower bounds are 49 and 57. The accompanying Lean project proves the required bounds and closed formal negations of both conjectures using standard group invariants. All 1024 conjugacy witnesses are checked by kernel reduction. The archive includes the paper and LaTeX, formal sources, certificates, pinned dependencies, Python verifiers, build and axiom reports, and reproduction instructions. AI assistance and the scope of the dated priority check are disclosed. Licenses by component: paper, original documentation and data, CC BY 4.0; original Lean and Python code, Apache-2.0.