Bass's determinant formula over a commutative ring

Bass's formula (1 - u²)^|V| · det(1 - u B) = (1 - u²)^|E| · det(1 - u A + u² (D - 1)) (B the Hashimoto matrix on darts, A the adjacency matrix, D the degree matrix) for every commutative ring R and every u : R. The identity is first obtained in ℤ[X]: its image in ℚ[X] is the field case bass_charpolyRev, and ℤ[X] → ℚ[X] is injective. Evaluating X ↦ u through ℤ → R then gives it in R.

Main results

• SimpleGraph.bass_determinant_commRing: Bass's determinant formula over any commutative ring

References

• C. Marín, Folding Edges into Vertices: A Machine-Checked Proof of Bass's Determinant Formula for the Ihara Zeta Function in Lean 4, Zenodo (2026), doi:10.5281/zenodo.20573120, thm:bass.

theorem SimpleGraph.bass_determinant_commRing {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (u : R) : (1 - u ^ 2) ^ Fintype.card V * (1 - u • G.hashimoto R).det = (1 - u ^ 2) ^ G.edgeFinset.card * (1 - u • adjMatrix R G + u ^ 2 • (degMatrix R G - 1)).det

Bass's determinant formula over any commutative ring (no field, no order on the vertices). (1 - u²)^|V| · det(1 - u B) = (1 - u²)^|E| · det(1 - u A + u² (D - 1)), where B is the Hashimoto (non-backtracking) matrix on darts, A the adjacency matrix and D the degree matrix. It is deduced from the field case bass_charpolyRev (over ℚ) by descending to ℤ[X] and evaluating.