Bounded elementary generation is not presently shorter. Nica's
[nica2019bounded, Theorem 2, p. 2] gives
\[\nu _3=\frac {3\cdot 3^2-3}{2}+29=41,\]
and its proof invokes the Kornblum–Artin theorem for irreducibles in
polynomial arithmetic progressions, stated as
[nica2019bounded, Theorem 3, p. 2]. That input is absent from the pinned
Mathlib revision.
Our internal estimate for a self-contained Nica–Kassabov
route is 20–45 thousand lines and three to six times the
current engineering effort, with roughly 70 percent internal uncertainty.
Assuming Kornblum–Artin gives our internal estimate of 8–15 thousand
lines, but merely moves the external boundary. Our internal estimate for a
reusable formalization of the generic EJK theorem is 45–90 thousand
lines; that generality is unnecessary for Zhou's application.
The route decomposition has four literature anchors:
- Zhou's exact invocation [zhou2026icc, Proposition 4.1, pp. 8–10];
- the elementary-group theorem, unweighted boundary graph, and packaged
six-root estimate [ershov2010noncommutative, Theorem 1.1, p. 1; Section 5.4, pp. 25–29;
Proposition 6.1, pp. 34–35];
- the broader root-graded theorem and arbitrary-ring relative estimate
[ershov2017rootgraded, Theorem 1.1, p. 3; Appendix Theorem A.1, p. 110];
and
- Kassabov's free-associative-ring estimates and Nica's exact-ring
alternative.
None states our LOC or effort ranges.