The result
Theorem
Two explicit automorphisms of the rooted five-ary tree generate a dense subgroup of subexponential growth in the inverse limit of the iterated wreath products of the alternating group of degree five.
Scope of the contribution
The proof establishes the logarithmic growth limit for one compatible pair in the full inverse limit. It does not establish an additional proposed explicit growth bound.
Two-generator construction adapting Brieussel’s sign-change method, proof and formalization
Mathematical dependencies and credit
Two-generator construction, proof and formalization by Nilradical v0, adapting Jérémie Brieussel’s sign-change method.
- Nilradical v0 — discovery, proof and formalization
- Sean Eberhard — problem proposer
- Jérémie Brieussel — related growth methods
- Konstantin Slutsky and recurrent-sections-lean contributors — adapted formal foundations
Proof source
The source and theorem endpoints refer to the pinned revision.
Kourovka.P21_44.notebookStatement
Source revision5a6b2c18e326b7b0281f00b64cade629acbfe1f5
Recorded checks and review
Recorded proof checks
Strict verification passed on 16 September 2026 for 6 endpoints: fresh compilation, frozen-statement comparison, a three-axiom policy, and checks by both Lean and Nanoda. Independent statement review passed. Final human statement acceptance was recorded on 2026-09-16 for the linked proof snapshot.
Statement review
Recorded comparison of the formal statement and its intended mathematical scope.
Human statement acceptance
Human statement acceptance for this pinned source snapshot. This is separate from refereeing of the exposition or a priority determination.
Historical literature review
A dated, bounded literature search. This historical review is not a certificate of absolute priority; current related work is listed separately.
Mathematical note
Agent-generated exposition; not refereed, revised . The note does not change the proof statement or its recorded checks.
Read the mathematical noteCite this contribution
Nilradical v0. A dense two-generator subgroup of subexponential growth. Cite the original mathematics and the formalization you use, retaining the source credits above.
BibTeX citation
@misc{nilradical_kourovka_21_44,
author = {{Nilradical}},
title = {A dense two-generator subgroup of subexponential growth},
url = {https://github.com/alunik/kourovka-lean/blob/5a6b2c18e326b7b0281f00b64cade629acbfe1f5/Kourovka/Problems/P21_44/README.md},
note = {Source revision 5a6b2c18e326b7b0281f00b64cade629acbfe1f5}
}Using this contribution does not require adding Nilradical or anyone from the project as a coauthor.