The Godsil–Gutman identity

The sum over all ±1 signings of the edges of G of the characteristic polynomials of the signed adjacency matrices is #signings • μ(G): the expected characteristic polynomial of a random signing is the matching polynomial.

The proof expands each determinant over permutations and exchanges the two sums. For a fixed permutation the sum over signings factors over edges, and an edge contributes 0 unless it is used an even number of times. The surviving permutations are the involutions whose 2-cycles are edges (SimpleGraph.IsEdgeInvolution); they correspond bijectively to the matchings of G, with sign (-1)^k for a k-edge matching.

Main results

• SimpleGraph.godsil_gutman: the Godsil–Gutman identity.
• SimpleGraph.innerSum_eq_ite: the sum over signings for a fixed permutation.
• SimpleGraph.permOfMatching, SimpleGraph.matchingOfPerm: the bijection between matchings and edge involutions.
• SimpleGraph.signAvg_ne_zero_iff: the average of a product of edge signs is nonzero iff every exponent is even.

References

• C. D. Godsil, I. Gutman, On the theory of the matching polynomial, J. Graph Theory 5 (1981) 137–144.
• A. W. Marcus, D. A. Spielman, N. Srivastava, Interlacing families I: Bipartite Ramanujan graphs of all degrees, Ann. of Math. 182 (2015) 307–325.

theorem SimpleGraph.signingMatrix_apply {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) (i j : V) : G.signingMatrix cfg i j = if G.Adj i j then if cfg s(i, j) = true then 1 else -1 else 0

Unfolding lemma for the signing matrix.

theorem SimpleGraph.signingMatrix_symm {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) (i j : V) : G.signingMatrix cfg i j = G.signingMatrix cfg j i

The signing matrix is symmetric — both the support (G.Adj) and the sign (Sym2 is unordered) are symmetric. Hence A_cfg is Hermitian over ℝ, so it has real eigenvalues (the input the spectral/Ramanujan side needs).

theorem SimpleGraph.signingMatrix_diag {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) (i : V) : G.signingMatrix cfg i i = 0

The diagonal of the signing matrix is zero (no self-loops).

theorem SimpleGraph.sum_signOf_eq_zero : (∑ b : Bool, if b = true then 1 else -1) = 0

The expectation seed. A single ±1 edge-sign averages to 0: ∑_{b} (±1) = 0. This is the engine of step 3 — it is why every term whose product contains an odd power of some edge-sign dies.

Steps 1–2: expand charpoly over permutations and read off the entries

theorem SimpleGraph.charmatrix_signingMatrix_diag {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) (i : V) : (G.signingMatrix cfg).charmatrix i i = Polynomial.X

Step 2 (fixed point). On the diagonal the char-matrix entry of the signing matrix is just X (the signing matrix has zero diagonal). So a fixed point of σ contributes a factor X.

theorem SimpleGraph.charmatrix_signingMatrix_offdiag {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) {i j : V} (h : i ≠ j) : (G.signingMatrix cfg).charmatrix i j = -Polynomial.C (G.signingMatrix cfg i j)

Step 2 (off-diagonal). Off the diagonal the char-matrix entry is −C of the signed adjacency entry. So a point in σ.support contributes −C (A_cfg)_{σ i, i}.

theorem SimpleGraph.charpoly_signingMatrix_eq_sum {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) : (G.signingMatrix cfg).charpoly = ∑ σ : Equiv.Perm V, ↑↑(Equiv.Perm.sign σ) * ∏ i : V, (G.signingMatrix cfg).charmatrix (σ i) i

Step 1. The characteristic polynomial of the signing matrix, expanded over permutations via Matrix.det_apply (charpoly = (charmatrix).det). The summand factorizes (step 2) into X^{#fixed} · ∏_{support} (−C …).

Step 3: split each permutation's product into X^{#fixed} · ∏_{support}(−C …)

theorem SimpleGraph.charmatrix_signingMatrix_factor {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) (σ : Equiv.Perm V) (i : V) : (G.signingMatrix cfg).charmatrix (σ i) i = if σ i = i then Polynomial.X else -Polynomial.C (G.signingMatrix cfg (σ i) i)

Step 2/3 (per factor). Each factor of the permutation product is X on a fixed point and −C (A_cfg)_{σ i, i} on the support.

theorem SimpleGraph.prod_charmatrix_split {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) (σ : Equiv.Perm V) : ∏ i : V, (G.signingMatrix cfg).charmatrix (σ i) i = Polynomial.X ^ {i : V | σ i = i}.card * ∏ i ∈ σ.support, -Polynomial.C (G.signingMatrix cfg (σ i) i)

Step 3 (product split). The permutation product factorizes into X over the fixed points times −C(A_cfg)_{σ i, i} over the support: ∏_i = X^{#fixed} · ∏_{i ∈ supp σ} (−C …).

Step 4 (first cut): only permutations whose support pairs are all edges survive

theorem SimpleGraph.prod_support_eq_zero_of_not_adj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) (σ : Equiv.Perm V) {i : V} (hi : i ∈ σ.support) (hni : ¬G.Adj (σ i) i) : ∏ j ∈ σ.support, -Polynomial.C (G.signingMatrix cfg (σ j) j) = 0

Step 4 (non-edge kills it). If some support pair (σ i, i) is NOT an edge of G, the support product is 0. So in ∑_σ, only permutations whose every support pair (σ j, j) is a G-edge can contribute — the first restriction toward "only edge-involutions (matchings) survive".

Step 5 (sign): an involution with k transpositions has sign (−1)^k

theorem SimpleGraph.sign_involution {V : Type u_1} [Fintype V] [DecidableEq V] (σ : Equiv.Perm V) (hσ : σ ^ 2 = 1) : Equiv.Perm.sign σ = (-1) ^ (σ.support.card / 2)

Step 5 (the sign). For an involution σ (σ² = 1), sign σ = (−1)^{#support / 2}. Since an edge-involution with k 2-cycles has #support = 2k, this is the (−1)^k weight that matches the matching polynomial's sign — obtained WITHOUT any cycleType multiset bookkeeping (sign_of_pow_two_eq_one + card_fixedPoints).

Assembly: swap the sums and isolate the inner config-sum S(σ)

theorem SimpleGraph.sum_charpoly_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∑ cfg : Sym2 V → Bool, (G.signingMatrix cfg).charpoly = ∑ σ : Equiv.Perm V, ↑↑(Equiv.Perm.sign σ) * (Polynomial.X ^ {i : V | σ i = i}.card * ∑ cfg : Sym2 V → Bool, ∏ i ∈ σ.support, -Polynomial.C (G.signingMatrix cfg (σ i) i))

Assembly step. Combining the permutation expansion (step 1) with the product split (step 3) and swapping ∑_cfg/∑_σ, the summed characteristic polynomial is a sum over permutations of sign σ • (X^{#fixed} · S(σ)), where S(σ) = ∑_cfg ∏_{support} (−C …) is the inner config-sum to be analyzed next (it vanishes unless σ is an edge-involution).

Analysis of S(σ): vanishes unless every support pair is an edge

theorem SimpleGraph.innerSum_eq_zero_of_not_adj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) {i : V} (hi : i ∈ σ.support) (hni : ¬G.Adj (σ i) i) : ∑ cfg : Sym2 V → Bool, ∏ j ∈ σ.support, -Polynomial.C (G.signingMatrix cfg (σ j) j) = 0

S(σ) analysis, first cut. If σ moves some vertex i to a non-neighbour ((σ i, i) not an edge), then the inner config-sum S(σ) is 0: every single configuration's support product already vanishes (prod_support_eq_zero_of_not_adj), so the sum over configurations is 0. Concept: a signed walk that steps along a non-edge carries weight 0, regardless of the signing.

theorem SimpleGraph.innerSum_eq_C {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) : ∑ cfg : Sym2 V → Bool, ∏ i ∈ σ.support, -Polynomial.C (G.signingMatrix cfg (σ i) i) = Polynomial.C (∑ cfg : Sym2 V → Bool, ∏ i ∈ σ.support, -G.signingMatrix cfg (σ i) i)

S(σ) reduces to a real-valued sum. Since C (the constant-polynomial embedding ℝ →+* ℝ[X]) is a ring hom, the whole ℝ[X]-valued inner sum S(σ) is C of a purely real quantity T'(σ) = ∑_cfg ∏_{support} (−A_cfg)_{σi,i}. This is the key reduction: the hard combinatorics (edge factorization, odd-multiplicity-vanishes) now happens in ℝ, where Finset.prod_univ_sum applies cleanly — no ℝ[X] machinery in the way. Concept: the polynomial structure was inert; the content is the real expectation of signed-edge-weight products.

Engine of the edge factorization: the per-edge ±1 power-sum (odd ↦ 0, even ↦ 2)

When T'(σ) is factorized over edges via Finset.prod_univ_sum, each edge e contributes the Bool-sum ∑_{b} (signOf b)^{mult(e)}, where mult(e) is how many support vertices map to e. These two lemmas give its value: 0 if the edge's multiplicity is odd, 2 if even. An odd multiplicity anywhere zeroes the whole product — this is precisely "every edge must be used an even number of times ⟺ σ² = 1".

theorem SimpleGraph.sum_signOf_pow_eq_zero_of_odd {k : ℕ} (hk : Odd k) : ∑ b : Bool, (if b = true then 1 else -1) ^ k = 0

Odd multiplicity ⟹ the per-edge ±1 power-sum vanishes (1^k + (−1)^k = 0 for odd k). The general form of sum_signOf_eq_zero (the k = 1 case).

theorem SimpleGraph.sum_signOf_pow_eq_two_of_even {k : ℕ} (hk : Even k) : ∑ b : Bool, (if b = true then 1 else -1) ^ k = 2

Even multiplicity ⟹ the per-edge ±1 power-sum is 2 (1^k + (−1)^k = 2 for even k). The surviving edges each contribute a factor 2, giving the overall 2^{#edges} normalization.

Fiberwise edge-factorization of the inner config-sum T'(σ)

The structural heart of step 3. Group the support product by the edge s(σ i, i) that each support vertex sits on (Finset.prod_fiberwise), then push ∑_cfg through ∏_e (Fintype.prod_sum): the inner real config-sum T'(σ) becomes a product over edges of a per-edge Bool-sum. This is what lets the "odd-multiplicity edge ⟹ 0" engine (sum_signOf_pow_eq_zero_of_odd) act edge by edge — each factor is a ∑_b over a fiber whose size is exactly that edge's multiplicity.

theorem SimpleGraph.innerSum_factor_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) : ∑ cfg : Sym2 V → Bool, ∏ i ∈ σ.support, -G.signingMatrix cfg (σ i) i = ∏ e : Sym2 V, ∑ b : Bool, ∏ i ∈ σ.support with s(σ i, i) = e, -if G.Adj (σ i) i then if b = true then 1 else -1 else 0

Per-edge collapse: each surviving edge contributes ∑_b (−signOf b)^{mult}

theorem SimpleGraph.sum_negSignOf_pow_eq_zero_of_odd {m : ℕ} (hm : Odd m) : ∑ b : Bool, (-if b = true then 1 else -1) ^ m = 0

The −signOf power-sum, odd case — the engine lemma in the sign that actually appears in innerSum_factor_edges. Same value as sum_signOf_pow_eq_zero_of_odd: the extra negation is absorbed by b ↦ ¬b (−(if true … )=−1, −(if false …)=1).

theorem SimpleGraph.sum_negSignOf_pow_eq_two_of_even {m : ℕ} (hm : Even m) : ∑ b : Bool, (-if b = true then 1 else -1) ^ m = 2

The −signOf power-sum, even case: value 2.

theorem SimpleGraph.fiber_prod_eq_pow {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (e : Sym2 V) (b : Bool) (he : ∀ i ∈ {i ∈ σ.support | s(σ i, i) = e}, G.Adj (σ i) i) : (∏ i ∈ σ.support with s(σ i, i) = e, -if G.Adj (σ i) i then if b = true then 1 else -1 else 0) = (-if b = true then 1 else -1) ^ {i ∈ σ.support | s(σ i, i) = e}.card

Fiber collapse. On an edge e all of whose support-fiber pairs (σ i, i) are genuine G-edges, the inner fiber product collapses to a single power: every factor equals −signOf b, so the product is (−signOf b)^{mult}, where mult is the fiber cardinality — exactly the multiplicity of e in σ's support walk. Feeding this into sum_negSignOf_pow_eq_* is what makes an odd-multiplicity edge zero the whole term.

The hard characterization: an odd edge-multiplicity exists ⟺ σ is not an involution

mult_σ(s(a,b)) = [σ a = b] + [σ b = a] ∈ {0,1,2}. It is odd (=1) exactly when σ sends a ↦ b but not b ↦ a, i.e. a lies on a cycle of length ≥ 3. Hence some pair has odd multiplicity ⟺ σ² ≠ 1. This lemma is the permutation-theoretic key step of the ⟹ direction: it produces the witnessing ordered edge a ↦ b ↦ (≠a).

theorem SimpleGraph.exists_of_sq_ne_one {V : Type u_1} [Fintype V] [DecidableEq V] (σ : Equiv.Perm V) (hσ : σ ^ 2 ≠ 1) : ∃ (a : V) (b : V), a ≠ b ∧ σ a = b ∧ σ b ≠ a

theorem SimpleGraph.fiber_witness {V : Type u_1} [Fintype V] [DecidableEq V] (σ : Equiv.Perm V) {a b : V} (hab : a ≠ b) (ha : σ a = b) (hb : σ b ≠ a) : {i ∈ σ.support | s(σ i, i) = s(a, b)} = {a}

The witness edge carries multiplicity 1. For the ordered edge a ↦ b with σ b ≠ a (the output of exists_of_sq_ne_one), the support-fiber over the unordered pair s(a, b) is exactly {a}: only a satisfies s(σ i, i) = s(a, b) (since b would need σ b = a). So this edge's multiplicity is 1 — odd — which is what makes its per-edge Bool-sum vanish.

theorem SimpleGraph.innerSum_factor_zero_of_sq_ne_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (hσ : σ ^ 2 ≠ 1) : ∑ cfg : Sym2 V → Bool, ∏ i ∈ σ.support, -G.signingMatrix cfg (σ i) i = 0

The hard direction's payoff: non-involutions contribute 0. If σ² ≠ 1, the inner config-sum T'(σ) vanishes. Proof: the witness edge s(a, c) (with σ a = c, σ c ≠ a) has fiber {a} (fiber_witness), so its per-edge factor is the single Bool-sum ∑_b −(if Adj then signOf b else 0), which is 0 (an odd, =1, multiplicity); one zero factor zeroes the whole edge-product (innerSum_factor_edges). This is precisely why only involutions (matchings) survive in ∑_σ.

The surviving value: edge-involutions give product 1 for every signing

theorem SimpleGraph.prod_eq_one_of_involution {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (cfg : Sym2 V → Bool) (σ : Equiv.Perm V) (hσ : σ ^ 2 = 1) (hedge : ∀ i ∈ σ.support, G.Adj (σ i) i) : ∏ i ∈ σ.support, -G.signingMatrix cfg (σ i) i = 1

Edge-involutions give product 1 for every signing. If σ² = 1 and every support pair is a G-edge, then for every configuration cfg the support product is 1. Pair each support vertex a with σ a (an involution on the support, Finset.prod_involution): the two factors of a 2-cycle are the same ±1 (by symmetry of the signing matrix), so their product is (±1)² = 1. Hence T'(σ) = ∑_cfg 1 = #configs for an edge-involution — the value that, weighted by sign = (−1)^k and X^{n−2k}, reassembles the matching polynomial.

theorem SimpleGraph.innerSum_eq_card_of_involution {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) (hσ : σ ^ 2 = 1) (hedge : ∀ i ∈ σ.support, G.Adj (σ i) i) : ∑ cfg : Sym2 V → Bool, ∏ i ∈ σ.support, -G.signingMatrix cfg (σ i) i = ↑(Fintype.card (Sym2 V → Bool))

The surviving value. For an edge-involution (σ² = 1, every support pair a G-edge) the inner config-sum T'(σ) equals #configs: the integrand is 1 for every signing (prod_eq_one_of_involution), so the sum is just the number of configurations. This is the constant that, summed against sign(σ)·X^{#fix(σ)} over the matchings, yields #configs • matchingPoly.

Assembly: the per-permutation trichotomy and the edge-involution predicate

theorem SimpleGraph.innerSum_zero_of_not_adj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) {i : V} (hi : i ∈ σ.support) (hni : ¬G.Adj (σ i) i) : ∑ cfg : Sym2 V → Bool, ∏ j ∈ σ.support, -G.signingMatrix cfg (σ j) j = 0

Non-edge support ⟹ T'(σ) = 0 (real level). If some support pair (σ i, i) is not a G-edge, every configuration's support product already contains a 0 factor, so T'(σ) = 0. Completes the trichotomy with innerSum_factor_zero_of_sq_ne_one (non-involution) and innerSum_eq_card_of_involution (edge-involution): only edge-involutions survive.

def SimpleGraph.IsEdgeInvolution {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (σ : Equiv.Perm V) : Prop

σ is an edge-involution: an involution (σ² = 1) all of whose 2-cycles are G-edges. These are exactly the permutations that survive ∑_cfg charpoly, and they biject with the matchings of G (a k-transposition edge-involution ↔ a k-edge matching).

Equations

• G.IsEdgeInvolution σ = (σ ^ 2 = 1 ∧ ∀ i ∈ σ.support, G.Adj (σ i) i)

@[instance_reducible]

instance SimpleGraph.instDecidableIsEdgeInvolution {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) : Decidable (G.IsEdgeInvolution σ)

Equations

• G.instDecidableIsEdgeInvolution σ = id inferInstance

theorem SimpleGraph.innerSum_eq_ite {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (σ : Equiv.Perm V) : ∑ cfg : Sym2 V → Bool, ∏ i ∈ σ.support, -G.signingMatrix cfg (σ i) i = if G.IsEdgeInvolution σ then ↑(Fintype.card (Sym2 V → Bool)) else 0

The trichotomy, collapsed. T'(σ) is #configs on edge-involutions and 0 on everything else. This is the per-permutation input to the final assembly: ∑_cfg charpoly = ∑_σ sign·X^{#fix}·C(T'(σ)) then collapses to a sum over edge-involutions only.

The bijection, inverse map: a matching M induces an involution σ_M

The hard half of the matching ↔ edge-involution bijection. Given a matching M (pairwise vertex-disjoint edges), the map partner M sends each matched vertex to the other endpoint of its (unique) edge and fixes everything else; it is an involution, hence a permutation permOfMatching.

theorem SimpleGraph.other'_congr {V : Type u_1} [DecidableEq V] {v : V} {z z' : Sym2 V} (p : v ∈ z) (q : v ∈ z') (hzz : z = z') : Sym2.Mem.other' p = Sym2.Mem.other' q

Sym2.Mem.other' depends only on the element and the edge, not on the membership proof: equal edges give equal partners.

theorem SimpleGraph.matching_unique_edge {V : Type u_1} [DecidableEq V] {M : Finset (Sym2 V)} (hM : IsMatchingSet M) {v : V} {e f : Sym2 V} (he : e ∈ M) (hf : f ∈ M) (hve : v ∈ e) (hvf : v ∈ f) : e = f

In a matching, the edge containing a given vertex is unique.

noncomputable def SimpleGraph.partner {V : Type u_1} [DecidableEq V] (M : Finset (Sym2 V)) (v : V) : V

The partner of v under matching M: the other endpoint of v's edge if matched, else v.

Equations

• SimpleGraph.partner M v = if h : ∃ e ∈ M, v ∈ e then Sym2.Mem.other' ⋯ else v

theorem SimpleGraph.partner_matched {V : Type u_1} [DecidableEq V] {M : Finset (Sym2 V)} (hM : IsMatchingSet M) {v : V} {e : Sym2 V} (heM : e ∈ M) (hve : v ∈ e) : partner M v = Sym2.Mem.other' hve

Value of partner at a matched vertex: the other endpoint of its edge (well-defined by uniqueness of the matching edge).

theorem SimpleGraph.partner_unmatched {V : Type u_1} [DecidableEq V] {M : Finset (Sym2 V)} {v : V} (h : ¬∃ e ∈ M, v ∈ e) : partner M v = v

theorem SimpleGraph.partner_involutive {V : Type u_1} [DecidableEq V] {M : Finset (Sym2 V)} (hM : IsMatchingSet M) : Function.Involutive (partner M)

partner M is an involution: matched vertices swap within their edge (Sym2.other_invol'), unmatched vertices are fixed.

noncomputable def SimpleGraph.permOfMatching {V : Type u_1} [DecidableEq V] {M : Finset (Sym2 V)} (hM : IsMatchingSet M) : Equiv.Perm V

The involution permutation induced by a matching.

Equations

• SimpleGraph.permOfMatching hM = Function.Involutive.toPerm (SimpleGraph.partner M) ⋯

@[simp]

theorem SimpleGraph.permOfMatching_apply {V : Type u_1} [DecidableEq V] {M : Finset (Sym2 V)} (hM : IsMatchingSet M) (v : V) : (permOfMatching hM) v = partner M v

theorem SimpleGraph.permOfMatching_sq {V : Type u_1} [DecidableEq V] {M : Finset (Sym2 V)} (hM : IsMatchingSet M) : permOfMatching hM ^ 2 = 1

permOfMatching is an involution.

theorem SimpleGraph.permOfMatching_isEdgeInvolution {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {M : Finset (Sym2 V)} (hM : IsMatchingSet M) (hMG : M ⊆ G.edgeFinset) : G.IsEdgeInvolution (permOfMatching hM)

When a matching's edges are edges of G, the induced involution is an edge-involution: every moved vertex is sent along a G-edge (the matching edge it lies on).

The bijection, forward map: an edge-involution σ induces a matching M(σ)

theorem SimpleGraph.edge_eq_of_mem {V : Type u_1} {σ : Equiv.Perm V} (hσ : σ ^ 2 = 1) {a v : V} (hv : v ∈ s(a, σ a)) : s(a, σ a) = s(v, σ v)

For an involution, a 2-cycle's edge is determined by any of its vertices: if v lies on the edge s(a, σ a), then that edge is s(v, σ v). (Either v = a, or v = σ a and then σ v = a.)

noncomputable def SimpleGraph.matchingOfPerm {V : Type u_1} [Fintype V] [DecidableEq V] (σ : Equiv.Perm V) : Finset (Sym2 V)

The matching induced by an edge-involution: the set of its 2-cycle edges {s(a, σ a) : a ∈ supp}.

Equations

• SimpleGraph.matchingOfPerm σ = Finset.image (fun (a : V) => s(a, σ a)) σ.support

theorem SimpleGraph.matchingOfPerm_subset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {σ : Equiv.Perm V} (h : G.IsEdgeInvolution σ) : matchingOfPerm σ ⊆ G.edgeFinset

M(σ)'s edges are edges of G (each 2-cycle pair is a G-edge).

theorem SimpleGraph.matchingOfPerm_isMatching {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {σ : Equiv.Perm V} (h : G.IsEdgeInvolution σ) : IsMatchingSet (matchingOfPerm σ)

M(σ) is a matching: its edges are pairwise vertex-disjoint, because for an involution any vertex determines its 2-cycle edge (edge_eq_of_mem).

The bijection is mutually inverse

theorem SimpleGraph.permOfMatching_matchingOfPerm {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {σ : Equiv.Perm V} (h : G.IsEdgeInvolution σ) : permOfMatching ⋯ = σ

Left inverse: recovering the edge-involution from its matching gives σ back. For each v: if v is moved, its M(σ)-edge is s(v, σ v) so its partner is σ v; if v is fixed, it is unmatched, so its partner is v = σ v.

theorem SimpleGraph.other'_ne {V : Type u_1} [DecidableEq V] {a : V} {z : Sym2 V} (hd : ¬z.IsDiag) (h : a ∈ z) : Sym2.Mem.other' h ≠ a

other' of a vertex on a non-diagonal edge differs from that vertex.

theorem SimpleGraph.matchingOfPerm_permOfMatching {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {M : Finset (Sym2 V)} (hM : IsMatchingSet M) (hMG : M ⊆ G.edgeFinset) : matchingOfPerm (permOfMatching hM) = M

Right inverse: the matching of the involution of a matching M (with M ⊆ G.edgeFinset) is M. ⊆: each 2-cycle edge s(a, partner a) reconstructs the matching edge through a. ⊇: each e ∈ M is a G-edge (non-diagonal), so any vertex a ∈ e is moved (its partner is the other, distinct, endpoint), and s(a, partner a) = e.

Card relation: support.card = 2 · |matching|

theorem SimpleGraph.fiber_card_two {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {σ : Equiv.Perm V} (h : G.IsEdgeInvolution σ) {e : Sym2 V} (he : e ∈ Finset.image (fun (a : V) => s(a, σ a)) σ.support) : {a ∈ σ.support | s(a, σ a) = e}.card = 2

Each edge of M(σ) has exactly two support preimages under a ↦ s(a, σ a): the two endpoints {b, σ b} of its 2-cycle.

theorem SimpleGraph.support_card_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {σ : Equiv.Perm V} (h : G.IsEdgeInvolution σ) : σ.support.card = 2 * (matchingOfPerm σ).card

The 2-to-1 count. For an edge-involution, the support has twice as many vertices as M(σ) has edges: supp.card = 2 · |M(σ)|. (Each matching edge is covered by its two endpoints.)

Final assembly

theorem SimpleGraph.charpoly_sum_eq_filter {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∑ cfg : Sym2 V → Bool, (G.signingMatrix cfg).charpoly = ∑ σ : Equiv.Perm V with G.IsEdgeInvolution σ, ↑↑(Equiv.Perm.sign σ) * Polynomial.X ^ {i : V | σ i = i}.card * Polynomial.C ↑(Fintype.card (Sym2 V → Bool))

Step 1: collapse to a sum over edge-involutions. Combining the permutation expansion (sum_charpoly_eq), the C-reduction (innerSum_eq_C) and the trichotomy (innerSum_eq_ite), ∑_cfg charpoly becomes a sum over the edge-involutions only, each contributing sign(σ)·X^{#fix}·C(#configs).

theorem SimpleGraph.intCast_units_neg_one_pow (k : ℕ) : ↑(↑(-1) ^ k) = (-1) ^ k

Casting (-1 : ℤˣ)^k through ℤ into ℝ[X] gives (-1)^k (the Units.val_pow rewrite is a no-op rfl, so we go by induction on the exponent).

theorem SimpleGraph.edgeInv_term {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {σ : Equiv.Perm V} (h : G.IsEdgeInvolution σ) : ↑↑(Equiv.Perm.sign σ) * Polynomial.X ^ {i : V | σ i = i}.card = Polynomial.C ((-1) ^ (matchingOfPerm σ).card) * Polynomial.X ^ (Fintype.card V - 2 * (matchingOfPerm σ).card)

Step A: per-term rewrite. For an edge-involution σ, its contribution sign(σ)·X^{#fix} equals C((−1)^{|M(σ)|})·X^{n−2|M(σ)|} — the term of the matching polynomial indexed by the matching M(σ). Uses sign_involution (=(−1)^{supp/2}), support_card_eq (supp=2|M|) and #fix = n−supp.

theorem SimpleGraph.matchingOfPerm_card_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {σ : Equiv.Perm V} (h : G.IsEdgeInvolution σ) : (matchingOfPerm σ).card ≤ Fintype.card V / 2

A matching of an edge-involution has at most n/2 edges (its 2|M| matched vertices fit in V).

theorem SimpleGraph.matchingOfPerm_mem {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {σ : Equiv.Perm V} (h : G.IsEdgeInvolution σ) : matchingOfPerm σ ∈ G.matchingsOfCard (matchingOfPerm σ).card

M(σ) is a |M(σ)|-edge matching of G.

theorem SimpleGraph.sum_filter_eq_sum_matchings {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∑ σ : Equiv.Perm V with G.IsEdgeInvolution σ, Polynomial.C ((-1) ^ (matchingOfPerm σ).card) * Polynomial.X ^ (Fintype.card V - 2 * (matchingOfPerm σ).card) = ∑ M ∈ G.edgeFinset.powerset with IsMatchingSet M, Polynomial.C ((-1) ^ M.card) * Polynomial.X ^ (Fintype.card V - 2 * M.card)

Step B: reindex the edge-involution sum to a sum over all matchings of G, via the bijection σ ↦ M(σ) / M ↦ σ_M.

theorem SimpleGraph.sum_matchings_eq_matchingPoly {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∑ M ∈ G.edgeFinset.powerset with IsMatchingSet M, Polynomial.C ((-1) ^ M.card) * Polynomial.X ^ (Fintype.card V - 2 * M.card) = G.matchingPoly

Step C: group by edge-count. The sum over all matchings, grouped by cardinality k, gives the matching polynomial (each size-k class contributes m_k copies of C((−1)^k)·X^{n−2k}).

The Godsil–Gutman identity (C2, complete)

theorem SimpleGraph.godsil_gutman {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.expected_charpoly_eq_matchingPoly_target

Godsil–Gutman (Component C2). The sum over all ±1 edge-signings of the characteristic polynomial of the signed adjacency matrix equals #configs • matchingPoly G. Equivalently, the expected characteristic polynomial of a uniformly random signing is the matching polynomial. This is the bridge from the spectral side to the combinatorial side of the Marcus–Spielman–Srivastava program.

Assembles: charpoly_sum_eq_filter (only edge-involutions survive) ∘ edgeInv_term (each contributes a matching-polynomial term) ∘ sum_filter_eq_sum_matchings (bijection) ∘ sum_matchings_eq_matchingPoly (group by edge-count).

The parity-closed-walk kernel (moment-level companion of Godsil–Gutman)

The algebraic heart of the identity P_d = 2^{−|E|} ∑_π trace(A_π^d) (Chen–van Dam–Bu 2023): a walk's signed weight, averaged over all ±1 signings, vanishes unless the walk is parity-closed (every edge used an even number of times). It is exactly our sign-killing engine sum_signOf_pow_* summed over edges via Fintype.prod_sum. Here t e is the edge-multiplicity of a walk; the product over signings of signOf(cfg e)^{t e} is 2^{#pairs} if all multiplicities are even, else 0.

theorem SimpleGraph.sum_signOf_prod_pow {V : Type u_1} [Fintype V] [DecidableEq V] (t : Sym2 V → ℕ) : ∑ cfg : Sym2 V → Bool, ∏ e : Sym2 V, (if cfg e = true then 1 else -1) ^ t e = if ∀ (e : Sym2 V), Even (t e) then 2 ^ Fintype.card (Sym2 V) else 0

The unifying principle: averaging over signings is the ℤ/2 parity projection

Both formalized results in this file are instances of one fact — averaging over all ±1 signings projects onto the parity-even part. Concretely (sum_signOf_prod_pow), ∑_cfg ∏_e signOf(cfg e)^{t e} is 2^{#pairs} when every multiplicity t e is even, and 0 otherwise. The "survives ⟺ even" gate (signAvg_ne_zero_iff) is the common heart of the two levels:

• Godsil–Gutman (godsil_gutman, characteristic-polynomial level): a permutation σ contributes to ∑_cfg charpoly(A_cfg) exactly when its support multiplicities are all even — i.e. σ² = 1, an involution, i.e. a matching. (Elementary-symmetric functions of the eigenvalues.)
• Parity-closed walks (Chen–van Dam–Bu 2023, moment level): a closed walk contributes to ∑_cfg trace(A_cfg^d) exactly when every edge is used an even number of times — a parity-closed walk. (Power sums of the eigenvalues.)

Elementary-symmetric (charpoly) and power-sum (moments) are two readings of the same ℤ/2-Fourier projection ∑_{s ∈ {±1}} s^k = 2·[k \text{ even}].

theorem SimpleGraph.signAvg_ne_zero_iff {V : Type u_1} [Fintype V] [DecidableEq V] (t : Sym2 V → ℕ) : ∑ cfg : Sym2 V → Bool, ∏ e : Sym2 V, (if cfg e = true then 1 else -1) ^ t e ≠ 0 ↔ ∀ (e : Sym2 V), Even (t e)

The parity gate. A sign-monomial survives the signing-average iff its multiplicity vector is even — the single principle underlying both godsil_gutman (where "even everywhere" = σ²=1, a matching) and the parity-closed-walk identity (where it = the walk is parity-closed).