Nonfreeness for rational two-parabolic groups with numerator 24

Abstract

This preprint presents a proof of nonfreeness for rational two-parabolic matrix groups with numerator 24. For every integer denominator r with |r| > 6, the groups at parameter 24/r are nonfree over both the rational and complex numbers, in SL(2,Q) and SL(2,C). For each such parameter, the proof provides a nonempty, freely reduced relation with at most 64 alternating nonzero generator-power syllables. For |r| > 17, the parameter is a two-step relation number. The mathematical results are accompanied by a Lean 4 and Mathlib formalization. This record includes the manuscript PDF and LaTeX sources, the complete Lean project with pinned dependencies, finite certificate data, an exact Python certificate verifier, and verification scripts and logs. The included verification documentation specifies the scope and provenance of the checks. Author: Ziheng Wang.AI assistance: GPT-6-Astra. The manuscript and its LaTeX/PDF sources are licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). The software and Lean sources are licensed separately under the MIT License. Source repository: https://github.com/wingsyuyi-satori/nonfree-G24r