The pinned Connes project uses Mathlib revision
c2d7843e
with Lean 4.34.0-rc2. 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
ac3bfb3
uses Mathlib ac1b4db
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-group, or magic-graph
lane. Recent
algebraic-group root-space additions
do not supply the root-graded-group criterion used by EJK. TauCeti is therefore
not a drop-in dependency for this boundary; aligning project pins would not
reduce the missing mathematics.