bibkey: gardam2021unitconjecture authors: Giles Gardam year: 2021 title: “A counterexample to the unit conjecture for group rings” doi: 10.4007/annals.2021.194.3.9 url: https://arxiv.org/abs/2102.11818v2 claim: “The Promislow group is torsion-free and its group ring over F_2 contains a unit that is not a group element.” strata_touched:

• D5/S3/ArithUnits/Gardam license: citation-only for the paper; transplanted proof source Apache-2.0 triage: anchor

Gardam’s counterexample to the unit conjecture

Giles Gardam, A counterexample to the unit conjecture for group rings, Annals of Mathematics 194 (3) (2021), arXiv:2102.11818v2, DOI 10.4007/annals.2021.194.3.9.

Theorem A uses the group P generated by a and b with relations b⁻¹ a² b a² = 1 and a⁻¹ b² a b² = 1. It defines x=a², y=b², z=(ab)² and an element u in the group ring F₂[P]. The formal module D5/S3/ArithUnits/Gardam checks all three clauses: every nonzero natural power equal to one forces the group element to be one, u is a unit, and u is not a basis group element.

Verified locator

Versioned arXiv record: https://arxiv.org/abs/2102.11818v2 . The published article is Annals of Mathematics 194 (3) (2021), DOI 10.4007/annals.2021.194.3.9.

The Lean source is a native transplantation of the accepted public source snapshot 92adfe225bb26dfed06f5ba77d9abbb7f680733f from trureturning-lean-eval, distributed under Apache-2.0. The implementation retains the exact presentation and coefficients, an explicit faithful four-coset normal form, the two-sided inverse certificate, and the 21-element support witness. It claims no new counterexample and does not replace the literature result.

Source boundary

The paper and its theorem are literature context. The repository truth anchor is the Lean module named above; the accepted benchmark submission is provenance for the transplanted code, not a separate mathematical claim.