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:
- quantitative Kazhdan subsets, constants, and relative ratios, with a
bridge to the current qualitative predicate; our internal allocation is
2–3.5 thousand lines;
- 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;
- fixed-space angles, codistance, and the class-two nilpotent estimate;
our internal allocation is 5–9 thousand;
- 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;
- 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
- 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.