The exact property-(T) input is classical and mathematically well established. The literature survey in [ershov2017rootgraded, Section 1.2, pp. 3–4] recalls that Kazhdan's 1967 theorem, together with subsequent work of Vaserstein, gives property (T) for \(G_\Phi (\mathbb F[t])=E_\Phi (\mathbb F[t])\) when \(\mathbb F\) is finite and \(\Phi \) is a reduced irreducible classical root system of rank at least two.

Taking \(\Phi =A_2\) and \(\mathbb F=\mathbb F_2\) yields the required \(E_{A_2}(\mathbb F_2[t])=\mathrm {EL}_3(\mathbb F_2[t])\) instance. The open boundary is therefore one of formalization completeness, not mathematical uncertainty.

The only remaining substantive premise is property (T) for \(\mathrm {EL}_3(\mathbb F_2[t])\). The route estimated below specializes the 2010 elementary-group theorem to \(R=\mathbb F_2[t]\) and \(n=3\). Its graph and six-root estimates are cited in the implementation layers below. The later root-graded treatment supplies broader supporting language.

Our central estimate remains 24–28 thousand new Lean lines; a wider plausible range is 18–35 thousand. That range is about \(0.8\)–\(1.5\) times the roughly 23,000 lines already in the project. We expect the proof search and engineering to require two to four times the effort of the present formalization.

This estimates one explicit, quantitative route that fits the present Lean interfaces; it is neither a measure of confidence in the theorem nor a lower bound for formalizing the classical route. The literature supports the route and its decomposition, not these LOC or effort figures.

The six implementation layers, with overlapping uncertainty ranges, are:

1. quantitative Kazhdan subsets, constants, and relative ratios, with a bridge to the current qualitative predicate; our internal allocation is 2–3.5 thousand lines;
2. the six additive root-subgroup embeddings and the direct \(A_2\) commutator relations; our internal allocation is 2–4 thousand. A Steinberg-group detour is optional, not required for this direct matrix-group specialization;
3. fixed-space angles, codistance, and the class-two nilpotent estimate; our internal allocation is 5–9 thousand;
4. the unweighted standard-Laplacian boundary case on six vertices. This is Section 5.4 of [ershov2010noncommutative]. Our internal allocation is 1.5–3 thousand; the weighted criterion in Section 5.5 is a separate generalization;
5. the packaged relative-ratio estimate for the union of all six root subgroups in [ershov2010noncommutative, Proposition 6.1, p. 34]; our internal allocation is 3–5.5 thousand. Six repeated Lean instantiations would be an implementation choice, not six mathematical inputs; and
6. assembly plus the exact qualitative export theorem for the elementary-group property-(T) boundary; our internal allocation is 1.5–3 thousand.

The allocations overlap. Their subtotal also excludes integration adapters, proof-search retries, and pin-specific repair risk, so it is not an arithmetic derivation of the 18–35 thousand-line envelope.

The existing analytic shell is not part of the missing estimate. Connes.spectral_criterion_unconditional already constructs the positive spectral functional and closes the scalar/PVM route from finite spectral detection to property (T).

The remaining work is the quantitative root-subgroup, fixed-space, graph, and detector mathematics listed above; it should reuse that shell rather than construct another PVM layer.

The pinned Connes project uses Mathlib revision 062f1e3d with Lean 4.34.0-rc1. Mathlib supplies the graph Laplacian and its positivity theorem, exposed by the declaration links above, but not the Ershov–Jaikin-Zapirain graph-of-groups criterion, Kazhdan ratios, root gradings, codistance, or the graph argument.

Kassabov's estimates for a free associative integer ring require quotient transport before application to \(\mathbb F_2[t]\) [kassabov2005universal, Theorem 2.2 and Lemmas 2.3–2.7]. For an arbitrary finitely generated ring and module, the cleaner calibration is [ershov2017rootgraded, Appendix Theorem A.1]. The direct route is the earlier quantitative development [ershov2010noncommutative, Sections 2–6 and Appendix A].

TauCeti at revision cc6ce75 uses Mathlib de5ce8a and Lean 4.34.0-rc1. Its diagonal-dominance proof consumes the same Mathlib Laplacian facts.

Its source and roadmap contain no direct property-(T), Kazhdan, codistance, root-graded, or magic-graph lane. It is therefore not a drop-in dependency for this boundary; aligning project pins would not reduce the missing mathematics.

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.

The cited literature formulates property (T) by quantifying over unitary representations. The basic definitions and elementary-group theorem appear in [ershov2010noncommutative, Section 3.1 and Theorem 1.1]; the root-graded generalization is [ershov2017rootgraded, Theorem 1.1]. Lean must also make the size of each carrier explicit.

The current Connes.HasKazhdanPropertyT takes a group in Type u and quantifies over Hilbert carriers in the same Type u. This conventional interface is sufficient for the theorem schema formalized here.

It matches the spectral consumer: spectral_criterion_unconditional is uniform in each K : Type u and each UnitaryRepresentation G K, rather than selecting one concrete \(\ell ^2\) or regular representation.

The interface does not assert universe independence. A classical theorem quantifying over carriers in every universe implies this predicate by restriction to Type u; thus EJZK safely supplies the premise used here. The converse is nontrivial and is not part of the present interface.

For a countable group, that converse has a two-stage route:

1. Choose witnesses for every finite subset and a cofinal sequence of positive accuracies. The closed span of their group orbits is invariant, complete, separable, and still has almost-invariant unit vectors. An invariant vector there remains invariant in the original representation.
2. Choose a countable Hilbert basis, reindex it by a small countable type, and conjugate the action onto the resulting \(\ell ^2\) carrier in the group's universe. The same-universe predicate then gives the polymorphic statement.

The pinned Mathlib already contains separability of spans (TopologicalSpace.IsSeparable.span), separability of closures (TopologicalSpace.IsSeparable.closure), completeness of closed spans (Submodule.topologicalClosure.completeSpace), and Hilbert-basis existence (exists_hilbertBasis).

At the pinned TauCeti revision, the continuous-representation library provides invariant restriction (TauCeti.ContRepresentation.subrepresentation), unitarity under restriction (TauCeti.ContRepresentation.IsUnitary.subrepresentation), and transport along an isometry (TauCeti.ContRepresentation.IsUnitary.congr).

Its compact-group lane also standardizes finite-dimensional carriers (TauCeti.IrrepModel) by an orthonormal basis, following the explicit finite-dimensional universe convention in its roadmap.

Neither pinned codebase assembles the countable invariant span, gives its Hilbert basis a small countable index, or transports the full property-(T) predicate across that model. Together these form the lowering seam.

They are more focused than generalizing the entire Connes.spectral_criterion_unconditional stack, but remain separate from closing the EJZK premise and from the present formalization.