Nilradical

Word maps over ℂ and ℝ

Kourovka Notebook · 16.68Answer: Complex affirmative; real negativeNilradical v1.0.0

The result

Complex theorem

Let K be an algebraically closed field of characteristic zero. Every nonidentity word w in the free group on two generators induces a surjective map w : PSL₂(K)² → PSL₂(K).

Real counterexample

There is an explicit nonidentity word W of cyclically reduced length 44 such that tr W(A, B) > 7/4 for every A, B ∈ SL₂(ℝ). Its word map on PSL₂(ℝ) is not surjective.

Scope of the contribution

The complex theorem holds over every algebraically closed field of characteristic zero. The real construction is a nonidentity word of length 44 whose values on SL₂(ℝ) have trace greater than 7/4. Lean proves omission of a specified projective involution and nonsurjectivity on PSL₂(ℝ); omission of all nonidentity involutions is a written consequence of the trace bound. The negative SO₃(ℝ) answer is due to Andreas Thom and is not formalized in these projects.

Complex surjectivity proof, real counterexample and formalization

Mathematical dependencies and credit

Complex proof, explicit real counterexample and formalizations by Nilradical v1.0.0. The complex proof uses Schneider–Thom’s elementary-matrix specialization and a polynomial-fibre observation of Mushkarov–Nikolov. The compact answer is Thom’s prior result.

  • Nilradical v1.0.0 — complex proof, real counterexample, formalization and verification
  • J. Mycielski — problem proposer
  • J. Schneider and A. Thom — elementary-matrix specialization
  • O. Mushkarov and N. Nikolov — polynomial-fibre observation
  • A. Thom — prior negative answer for SO₃(ℝ)
  • Lean and mathlib contributors — formal foundations

Proof source

The source and theorem endpoints refer to the pinned revision.

  • WordMaps.word_surjective
  • WordMaps.complex_word_surjective
  • RealWord.tr_value_gt_seven_fourths
  • RealWord.word_ne_one
  • RealWord.word_not_surjective
  • RealWord.exists_nontrivial_nonsurjective_word

Source revision
75b93ec1363f5ba4d138512a9dba13f749855f4e

Proof sourceReal Lean sourceProof overview

Recorded checks and review

Recorded proof checks

Both frozen projects passed protected verification with statement comparison, the three-axiom policy, Lean and Nanoda. The complex run checked two declarations and the real run checked fifteen. No SO₃ proof or separate all-involution endpoint is included. Final human statement acceptance was recorded on 2026-09-21 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 dated review distinguishes the two published developments from established special cases and ingredients. Thom’s compact result is prior work. 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. Word maps over ℂ and ℝ. Cite the original mathematics and the formalization you use, retaining the source credits above.

BibTeX citation
@misc{nilradical_kourovka_16_68,
  author = {{Nilradical}},
  title = {Word maps over ℂ and ℝ},
  url = {https://github.com/alunik/kourovka-lean/blob/d677596183f8c4ac538d692ab03c80005d1f15d5/Kourovka/Problem1668/README.md},
  note = {Source revision 75b93ec1363f5ba4d138512a9dba13f749855f4e}
}

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