The Ihara trace generating function

Combining Bass's determinant formula with Jacobi's formula and Newton's identity for traces (Matrix.derivative_coe_charpolyRev), the generating function ∑ₖ tr(Bᵏ⁺¹) Xᵏ of the traces of the powers of the non-backtracking operator B is expressed through the adjacency and degree matrices. The traces tr(Bᵏ) count closed non-backtracking walks of length k.

Main results

• SimpleGraph.trace_adjMatrix_pow: tr(Aᵏ) is the number of closed walks of length k.
• SimpleGraph.bass_charpolyRev: Bass's formula as an identity in R[X].
• SimpleGraph.derivative_bass: its derivative (Jacobi's formula on both sides).
• SimpleGraph.ihara_Nk_isolated, SimpleGraph.ihara_Nk_explicit: the generating function of tr(Bᵏ⁺¹) in terms of A and D.
• SimpleGraph.ihara_Nk_genfn: d⁄dX (charpolyRev B) = - charpolyRev B · ∑ₖ tr(Bᵏ⁺¹) Xᵏ.

References

• H. Bass, The Ihara–Selberg zeta function of a tree lattice, Internat. J. Math. 3 (1992) 717–797.
• A. Terras, Zeta Functions of Graphs: A Stroll through the Garden, Cambridge University Press, 2011.

The trace generating function

A general-matrix interlude, independent of graphs. The resolvent series ∑ₖ Mᵏ Xᵏ, viewed as a matrix of formal power series, is the formal inverse of 1 - X•M, and its trace is the trace generating function ∑ₖ tr(Mᵏ) Xᵏ. Everything here is eigenvalue-free and over an arbitrary CommRing — the half of the Newton/trace-generating-function bridge that needs no determinant. The determinant half is Jacobi's formula (det F)′ = tr(adj F · F′), proved below in derivative_det; together they will tie the trace power sums to charpolyRev and so to Bass's identity (bass_charpolyRev).

theorem SimpleGraph.trace_adjMatrix_pow {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : (adjMatrix ℕ G ^ k).trace = ∑ v : V, (G.finsetWalkLength k v v).card

Piece 1 of the trace formula. The trace of the k-th power of the adjacency matrix counts the closed walks of length k: tr(Aᵏ) = Σ_v #{closed walks of length k at v}.

theorem SimpleGraph.bass_charpolyRev {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [Field R] [Infinite R] [LinearOrder V] : (1 - Polynomial.X ^ 2) ^ Fintype.card V * (1 - Polynomial.X • (G.hashimoto R).map ⇑Polynomial.C).det = (1 - Polynomial.X ^ 2) ^ G.edgeFinset.card * (1 - Polynomial.X • (adjMatrix R G).map ⇑Polynomial.C + Polynomial.X ^ 2 • (degMatrix R G - 1).map ⇑Polynomial.C).det

Piece 2 — Bass as a polynomial identity (the charpoly form). Lifting bass_determinant (pointwise over an infinite field) to an identity in R[X], with the non-backtracking side expressed through Matrix.charpolyRev B = det(1 - X•B). This is the foundation for extracting the non-backtracking trace counts N_k = tr(Bᵏ) from the adjacency data.

theorem SimpleGraph.derivative_bass {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [Field R] [Infinite R] [LinearOrder V] : Polynomial.derivative ((1 - Polynomial.X ^ 2) ^ Fintype.card V) * (1 - Polynomial.X • (G.hashimoto R).map ⇑Polynomial.C).det + (1 - Polynomial.X ^ 2) ^ Fintype.card V * ((1 - Polynomial.X • (G.hashimoto R).map ⇑Polynomial.C).adjugate * (1 - Polynomial.X • (G.hashimoto R).map ⇑Polynomial.C).map ⇑Polynomial.derivative).trace = Polynomial.derivative ((1 - Polynomial.X ^ 2) ^ G.edgeFinset.card) * (1 - Polynomial.X • (adjMatrix R G).map ⇑Polynomial.C + Polynomial.X ^ 2 • (degMatrix R G - 1).map ⇑Polynomial.C).det + (1 - Polynomial.X ^ 2) ^ G.edgeFinset.card * ((1 - Polynomial.X • (adjMatrix R G).map ⇑Polynomial.C + Polynomial.X ^ 2 • (degMatrix R G - 1).map ⇑Polynomial.C).adjugate * (1 - Polynomial.X • (adjMatrix R G).map ⇑Polynomial.C + Polynomial.X ^ 2 • (degMatrix R G - 1).map ⇑Polynomial.C).map ⇑Polynomial.derivative).trace

The differentiated Bass identity — composing Bass with Jacobi (lemma 1). Applying d/dX to Bass's determinant formula and expanding both determinant derivatives by Jacobi's formula (Matrix.derivative_det): the non-backtracking side (1-X²)^|V|·det(1-X·B) and the adjacency side (1-X²)^|E|·det(1-X·A+X²(D-1)) have equal derivatives, term by term. This is the polynomial heart of the Ihara N_k spectral formula — the trace generating functions arise on dividing through by the two determinants (both units in R⟦X⟧).

theorem SimpleGraph.ihara_Nk_isolated {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [Field R] [Infinite R] [LinearOrder V] : (↑((1 - Polynomial.X ^ 2) ^ Fintype.card V) * ↑(1 - Polynomial.X • (G.hashimoto R).map ⇑Polynomial.C).det * PowerSeries.mk fun (k : ℕ) => (G.hashimoto R ^ (k + 1)).trace) = ↑(1 - Polynomial.X • (G.hashimoto R).map ⇑Polynomial.C).det * PowerSeries.derivative ↑((1 - Polynomial.X ^ 2) ^ Fintype.card V) - ↑((1 - Polynomial.X ^ 2) ^ G.edgeFinset.card) * PowerSeries.derivative ↑(1 - Polynomial.X • (adjMatrix R G).map ⇑Polynomial.C + Polynomial.X ^ 2 • (degMatrix R G - 1).map ⇑Polynomial.C).det - ↑(1 - Polynomial.X • (adjMatrix R G).map ⇑Polynomial.C + Polynomial.X ^ 2 • (degMatrix R G - 1).map ⇑Polynomial.C).det * PowerSeries.derivative ↑((1 - Polynomial.X ^ 2) ^ G.edgeFinset.card)

The isolated Ihara N_k identity (cleared form). Differentiating Bass's identity in R⟦X⟧ and substituting Newton's identity for matrix traces (Matrix.derivative_coe_charpolyRev) on the non-backtracking side isolates the N_k = tr(Bᵏ) generating function, expressed through the adjacency data Q = det(1 - X·A + X²(D-1)): (1-X²)^|V| · det(1-X·B) · ∑ₖ tr(Bᵏ⁺¹)Xᵏ = det(1-X·B)·((1-X²)^|V|)′ - (1-X²)^|E|·Q′ - Q·((1-X²)^|E|)′. The two (1-X²)-powers and the determinants are units in R⟦X⟧, so dividing through gives the generating function ∑ₖ N_{k+1} Xᵏ purely in terms of the adjacency spectrum.

theorem SimpleGraph.ihara_Nk_explicit {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [Field R] [Infinite R] [LinearOrder V] : (PowerSeries.mk fun (k : ℕ) => (G.hashimoto R ^ (k + 1)).trace) = (↑((1 - Polynomial.X ^ 2) ^ Fintype.card V) * ↑(1 - Polynomial.X • (G.hashimoto R).map ⇑Polynomial.C).det).invOfUnit 1 * (↑(1 - Polynomial.X • (G.hashimoto R).map ⇑Polynomial.C).det * PowerSeries.derivative ↑((1 - Polynomial.X ^ 2) ^ Fintype.card V) - ↑((1 - Polynomial.X ^ 2) ^ G.edgeFinset.card) * PowerSeries.derivative ↑(1 - Polynomial.X • (adjMatrix R G).map ⇑Polynomial.C + Polynomial.X ^ 2 • (degMatrix R G - 1).map ⇑Polynomial.C).det - ↑(1 - Polynomial.X • (adjMatrix R G).map ⇑Polynomial.C + Polynomial.X ^ 2 • (degMatrix R G - 1).map ⇑Polynomial.C).det * PowerSeries.derivative ↑((1 - Polynomial.X ^ 2) ^ G.edgeFinset.card))

The explicit Ihara N_k generating function. Dividing ihara_Nk_isolated through by the unit (1-X²)^|V|·det(1-X·B) (constant term 1, inverted by PowerSeries.invOfUnit) yields the non-backtracking trace power sums ∑ₖ tr(Bᵏ⁺¹) Xᵏ explicitly in terms of the adjacency spectrum.

theorem SimpleGraph.ihara_Nk_genfn {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] : PowerSeries.derivative ↑(G.hashimoto R).charpolyRev = -↑(G.hashimoto R).charpolyRev * PowerSeries.mk fun (k : ℕ) => (G.hashimoto R ^ (k + 1)).trace

The Ihara N_k generating function. Specialising Newton's identity for matrix traces (Matrix.derivative_coe_charpolyRev) to the Hashimoto non-backtracking operator B = G.hashimoto R: the logarithmic derivative of the reciprocal Ihara zeta det(1 - X·B) = charpolyRev B generates the non-backtracking closed-walk counts N_{k+1} = tr(B^{k+1}), (det(1 - X·B))′ = -det(1 - X·B) · ∑ₖ N_{k+1} Xᵏ.