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.