EJZK route and effort estimate [connes-000B]
✍️source
elementaryGroup
L∃∀N
SimpleGraph.lapMatrix
L∃∀N

    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.