The diameter of U(3,ℤ/mℤ) with respect to the fundamental roots is 2⌊ m/2⌋ for every m ≥ 8
Abstract
Let U(3,ℤ/mℤ) be the group of upper unitriangular 3 × 3 matrices over ℤ/mℤ, and let its Cayley graph be taken with respect to the four fundamental-root generators I ± E₁₂, I ± E₂₃. The CayleyPy collaboration (arXiv:2509.19162) computed the diameter of this graph for m=8,…,50, found it to be 2⌊ m/2⌋ throughout that range, and conjectured (their Conjecture 8) that, for the undirected Cayley graph on the fundamental roots, the diameter of U(n,ℤ/mℤ) equals (n-1)⌊ m/2⌋ for all large enough m, without naming a threshold. We prove the case n=3 of that conjecture for every m ≥ 8: every element of U(3,ℤ/mℤ) is a product of at most 2⌊ m/2⌋ generators, and the element (⌊ m/2⌋,⌊ m/2⌋,0) needs that many. The upper bound is an explicit lattice-path construction — one horizontal excursion carrying a prescribed number of up- and down-steps — together with a three-case arithmetic inequality; it involves no computation over m. The threshold 8 is sharp: at m=7 the element (0,0,3) is not a product of six generators, which is checked by enumerating all 5461 words of length at most six. Every statement is machine-checked in Lean 4 over Mathlib, with the standard axioms only.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
0b755898269a299d1ae86cfdbfdd3a779cbda0e6e25b36f23e8c9c1195321374
Claim ledger
Stated results
HD1candidate2026-09-03
upper bound, every modulus m >= 8: every element of U(3, Z/mZ) is a product of at most 2*floor(m/2) of the four fundamental-root generators E +- E₁₂, E +- E₂₃; proved by an explicit lattice-path construction (one horizontal excursion of width W = max(A, floor(floor(m/2)/2)) carrying g up- and g' down-steps), not by any computation over m
HD2known2026-09-03
lower bound, every modulus m: the element (floor(m/2), floor(m/2), 0) of U(3, Z/mZ) is not a product of fewer than 2*floor(m/2) fundamental-root generators, because its image in the abelianization (Z/mZ)² already is not
HD3candidate2026-09-03
the n = 3, fundamental/undirected case of Conjecture 8 of arXiv:2509.19162v2, with a sharp threshold: for every m >= 8 the diameter of the Cayley graph of U(3, Z/mZ) with respect to the four generators E +- E₁₂, E +- E₂₃ equals exactly 2*floor(m/2)
HD4routine2026-09-03
negative control refuting a too-small value: at m = 8 the element (4, 4, 0) of U(3, Z/8Z) is not a product of 7 generators, so diam U(3, Z/8Z) <= 7 is false
HD5routine2026-09-03
the threshold m >= 8 is sharp and the hypothesis is not vacuous: at m = 7 the element (0, 0, 3) of U(3, Z/7Z) is not a product of 6 = 2*floor(7/2) generators, so diam U(3, Z/7Z) is not 2*floor(7/2); checked in the kernel by enumerating all 1 + 4 +... + 4⁶ = 5461 words of length at most 6
HD6routine2026-09-03
positive controls: diam U(3, Z/8Z) = 8 and diam U(3, Z/100Z) = 100 as instances of the exact-value theorem, and the bound is attained – (4, 4, 0) IS a product of 8 generators in U(3, Z/8Z)
HD7known data2026-09-03
computed diameter table: diam U(3, Z/mZ) = 2*floor(m/2) for m = 1 and for every 8 <= m <= 400, and = 2*floor(m/2) + 2 for every 2 <= m <= 7; the diameter-attaining elements are (floor(m/2), floor(m/2), *) together with (0, 0, c) for c near m/2, and for m >= 12 only the former
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- U(3, Z/mZ) is the group of upper unitriangular 3 x 3 matrices over Z/mZ — the mod-m Heisenberg group. Writing I + a E₁2 + b E₂3 + c E₁3 as the triple (a, b, c), the group law is
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7