Alternative EJZK routes and literature anchors [connes-000I]

✍️source

elementaryGroup

L∃∀NAGENTDRAFTED

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.