Nilradical

Preserving product orders 2 and 3 is not enough

Kourovka Notebook · 21.53Answer: NegativeNilradical v1.0.0

The result

Counterexample

In a finite nonabelian simple matrix group over GF(8), swapping two involutions of a conjugacy class and fixing the others preserves every product of order 2 or 3 but sends a product of order 5 to one of order 7.

Scope of the contribution

A counterexample to the universal assertion, acting on the whole involution class in a concrete nonabelian finite simple matrix group. Simplicity and the two smallest prime divisors, 2 and 3, are proved directly; no identification with a named Ree group or exact group order is assumed.

Whole-class counterexample, proof and formalization

Mathematical dependencies and credit

Counterexample, proof, Lean formalization and verification by Nilradical v1.0.0. The group constructions and structural ingredients are prior mathematics credited in the proof record; reused formal foundations retain their source credits.

  • Nilradical v1.0.0 — counterexample, proof, formalization and verification
  • I. B. Gorshkov — original question
  • R. A. Wilson and K. Coolsaet — prior matrix group constructions
  • TauCeti contributors — reused abstract Tits-system and Bruhat proofs
  • mathlib contributors — formal foundations

Proof source

The source and theorem endpoints refer to the pinned revision.

  • Kourovka.Problem2153.not_statement

Source revision
fab8915562b0b7202ae4c1c7d7765c4bd8e616ea

Proof sourceProof overview

Recorded checks and review

Recorded proof checks

Protected comparison, the three-axiom audit, and checks by Lean and Nanoda passed for the frozen endpoint. The Auckland replay passed all 159 modules in its complete dependency closure. This was not a fresh full-repository build. The execution used workflow 0.4.0-draft. Independent mathematics and statement reviews passed. Final human statement acceptance was recorded on 2026-09-17 for the linked proof snapshot.

Recorded proof checks record

Statement review

Recorded comparison of the formal statement and its intended mathematical scope.

Statement review record

Human statement acceptance

Human statement acceptance for this pinned source snapshot. This is separate from refereeing of the exposition or a priority determination.

Human statement acceptance record

Historical literature review

The publication-time refresh found no new lead preventing release and left the accepted 16 September bounded contribution wording unchanged. No absolute priority claim is made.

Historical literature review record

Mathematical note

Agent-generated exposition; not refereed, revised . The note does not change the proof statement or its recorded checks.

Read the mathematical note

Cite this contribution

Nilradical v1.0.0. Preserving product orders 2 and 3 is not enough. Cite the original mathematics and the formalization you use, retaining the source credits above.

BibTeX citation
@misc{nilradical_kourovka_21_53,
  author = {{Nilradical}},
  title = {Preserving product orders 2 and 3 is not enough},
  url = {https://github.com/alunik/kourovka-lean/blob/4c13da19c50b417e48ff2431a6ea76edade3eb81/Kourovka/Problem2153/README.md},
  note = {Source revision fab8915562b0b7202ae4c1c7d7765c4bd8e616ea}
}

Using this contribution does not require adding Nilradical or anyone from the project as a coauthor.