The path-ends derivative does not minimize Kemeny’s edge derivative

Abstract

A connected barbell on 23 vertices has a smaller Kemeny edge derivative than the path.

The edge weight varies by a real parameter t, and weighted degrees vary with it. Kemeny’s constant is the sum of reciprocals of the nonzero eigenvalues of the normalized Laplacian, counted with multiplicity.

Definition 1.1 (One-edge perturbation).

$$\forall n\in \mathrm{Nat},\forall G\in \mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)]\forall a\in \mathrm{Fin}\left(n\right),\forall b\in \mathrm{Fin}\left(n\right),\forall t\in \mathrm{Real},\mathrm{paramAdj}\left(G,a,b,t\right)=\mathrm{SimpleGraph}.\mathrm{adjMatrix}\left(G,\mathrm{Real}\right)+t\cdot (\mathrm{Matrix}.\mathrm{single}\left(a,b,1\right)+\mathrm{Matrix}.\mathrm{single}\left(b,a,1\right))$$

Formalization. D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.paramAdj (✓ std3).

Citation. C. Albright; K. P. Hadaway; A. H. Pomerance; J. Jeffries; K. J. Lorenzen; A. K. Nix (2023). On the Edge Derivative of the Normalized Laplacian with Applications to Kemeny’s Constant. DOI: 10.48550/arXiv.2211.01495. URL: https://arxiv.org/abs/2211.01495v2.

Commentary.

Section 2, page 3, states: “Aksoy et al. in [2] represented M(t) = A + tB where A is the adjacency matrix of a graph G and B is a symmetric matrix representing a collection of edges.” It continues: “We will not restrict B and instead have B be a symmetric matrix representing any collection of edges denoted EC.” Section 1, page 3, states: “Here, we assume all unweighted edges have weight 1 and all non-edges have weight 0.” For vertices a and b, B is the sum of the two matrix units at (a,b) and (b,a); the vertex set is Fin n.

Definition 1.2 (Normalized Laplacian).

$$\forall n\in \mathrm{Nat},\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathrm{Real}\right),\mathrm{normLap}\left(A\right)=1-\mathrm{Matrix}.\mathrm{of}\left(\mathrm{fun}i:\mathrm{Fin}\left(n\right)\mapsto \mathrm{fun}j:\mathrm{Fin}\left(n\right)\mapsto \frac{A\left(i,j\right)}{\mathrm{Real}.\mathrm{sqrt}\left({\sum }_{k:\mathrm{Fin}\left(n\right)}A\left(i,k\right)\right)\cdot \mathrm{Real}.\mathrm{sqrt}\left({\sum }_{k:\mathrm{Fin}\left(n\right)}A\left(j,k\right)\right)}\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.normLap (✓ std3).

Citation. C. Albright; K. P. Hadaway; A. H. Pomerance; J. Jeffries; K. J. Lorenzen; A. K. Nix (2023). On the Edge Derivative of the Normalized Laplacian with Applications to Kemeny’s Constant. DOI: 10.48550/arXiv.2211.01495. URL: https://arxiv.org/abs/2211.01495v2.

Commentary.

Section 1, page 3, states: “The normalized Laplacian matrix of a graph is given by L = I − D^{−1/2} A D^{−1/2} where A is the adjacency matrix and D is the degree diagonal matrix.” The displayed entries use the row sums of A for those degrees, including for the perturbed adjacency matrix.

Definition 1.3 (Kemeny’s constant).

$$\forall n\in \mathrm{Nat},\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathrm{Real}\right),\mathrm{kemeny}\left(A\right)=\mathrm{Multiset}.\mathrm{sum}\left(\mathrm{Multiset}.\mathrm{map}\left(\mathrm{fun}x:\mathrm{Real}\mapsto x^{-1},\mathrm{Multiset}.\mathrm{filter}\left(\mathrm{fun}x:\mathrm{Real}\mapsto x\ne 0,\mathrm{Polynomial}.\mathrm{roots}\left(\mathrm{Matrix}.\mathrm{charpoly}\left(\mathrm{normLap}\left(A\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.kemeny (✓ std3).

Citation. C. Albright; K. P. Hadaway; A. H. Pomerance; J. Jeffries; K. J. Lorenzen; A. K. Nix (2023). On the Edge Derivative of the Normalized Laplacian with Applications to Kemeny’s Constant. DOI: 10.48550/arXiv.2211.01495. URL: https://arxiv.org/abs/2211.01495v2.

Commentary.

Section 1, page 3, states: “Kemeny’s constant can be computed as” K(G) = Σ_{λT ≠ 1} 1/(1 − λT) = Σ_{λL ≠ 0} 1/λL, “where each λL is an eigenvalue of L.” The encoding filters the multiset of real characteristic roots by nonzeroness, maps inversion, and sums. For the real symmetric normalized Laplacians in the proof, these roots are the eigenvalues with multiplicity.

Definition 1.4 (Reciprocal nonzero characteristic roots).

$$\forall I\in \mathrm{Type},[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall L\in \mathrm{Matrix}\left(I,I,\mathrm{Real}\right),\mathrm{reciprocalRoots}\left(L\right)=\mathrm{Multiset}.\mathrm{sum}\left(\mathrm{Multiset}.\mathrm{map}\left(\mathrm{fun}x:\mathrm{Real}\mapsto x^{-1},\mathrm{Multiset}.\mathrm{filter}\left(\mathrm{fun}x:\mathrm{Real}\mapsto x\ne 0,\mathrm{Polynomial}.\mathrm{roots}\left(\mathrm{Matrix}.\mathrm{charpoly}\left(L\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.reciprocalRoots (✓ std3).

Source. Repository-derived.

Commentary.

For any finite index type, the characteristic-root multiset is filtered by nonzeroness, inverted and summed. Real inversion at zero is zero.

Theorem 1.5 (The spectral reciprocal sum).

$$\forall I\in \mathrm{Type},[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall L\in \mathrm{Matrix}\left(I,I,\mathrm{Real}\right),\forall hL\in \mathrm{Matrix}.\mathrm{IsHermitian}\left(L\right),\mathrm{reciprocalRoots}\left(L\right)=\sum _{i:I}\mathrm{hL}.\mathrm{eigenvalues}{\left(i\right)}^{-1}$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.reciprocalRoots_eq_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a real Hermitian matrix, the characteristic-root multiset agrees with its real eigenvalues counted with multiplicity.

Theorem 1.6 (A generalized inverse trace).

$$\forall I\in \mathrm{Type},[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall L\in \mathrm{Matrix}\left(I,I,\mathrm{Real}\right),\forall P\in \mathrm{Matrix}\left(I,I,\mathrm{Real}\right),\forall T\in \mathrm{Matrix}\left(I,I,\mathrm{Real}\right),(\mathrm{Matrix}.\mathrm{IsHermitian}\left(L\right))\Rightarrow (((L)\cdot (T)=1-P)\Rightarrow (((L)\cdot (P)=0)\Rightarrow (((P)\cdot (T)=0)\Rightarrow (\mathrm{reciprocalRoots}\left(L\right)=\mathrm{Matrix}.\mathrm{trace}\left(T\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.reciprocalRoots_eq_trace (✓ std3). ∎

Source. Repository-derived.

Commentary.

The three displayed matrix equations identify the reciprocal sum with the trace of T. This statement concerns arbitrary real Hermitian matrices and does not assume a normalized Laplacian.

Definition 1.7 (Conjecture 3.5: minimality).

$$\mathrm{claim}=(\forall n\in \mathrm{Nat},(2\le n)\Rightarrow (\forall G\in \mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)]\forall a\in \mathrm{Fin}\left(n\right),\forall b\in \mathrm{Fin}\left(n\right),\forall dG\in \mathrm{Real},\forall dP\in \mathrm{Real},(\mathrm{SimpleGraph}.\mathrm{Connected}\left(G\right))\Rightarrow ((a\ne b)\Rightarrow ((\mathrm{HasDerivAt}\left(\mathrm{fun}t:\mathrm{Real}\mapsto \mathrm{kemeny}\left(\mathrm{paramAdj}\left(G,a,b,t\right)\right),dG,0\right))\Rightarrow ((\mathrm{HasDerivAt}\left(\mathrm{fun}t:\mathrm{Real}\mapsto \mathrm{kemeny}\left(\mathrm{paramAdj}\left(\mathrm{SimpleGraph}.\mathrm{pathGraph}\left(n\right),⟨0⟩,⟨n-1⟩,t\right)\right),dP,0\right))\Rightarrow (dP\le dG))))))$$

Formalization. D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.claim (✓ std3).

Citation. C. Albright; K. P. Hadaway; A. H. Pomerance; J. Jeffries; K. J. Lorenzen; A. K. Nix (2023). On the Edge Derivative of the Normalized Laplacian with Applications to Kemeny’s Constant. DOI: 10.48550/arXiv.2211.01495. URL: https://arxiv.org/abs/2211.01495v2.

Commentary.

Conjecture 3.5, page 19, states verbatim: “For a given n, the derivative of Kemeny’s constant on simple graphs of order n is smallest on the path on n vertices with respect to the non-edge connecting the ends of the path. The value of this derivative is O(n³).” The proposition expresses the first sentence for connected graphs on Fin n with n ≥ 2 and a ≠ b. Both derivatives must exist at zero. The path endpoints are the elements of Fin n with values 0 and n − 1; the inequality n ≥ 2 supplies their bounds. The second sentence concerns growth of the path value and is outside this proposition.

Theorem 1.8 (A strict counterexample at order 23).

$$\neg (\forall n\in \mathrm{Nat},(2\le n)\Rightarrow (\forall G\in \mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)]\forall a\in \mathrm{Fin}\left(n\right),\forall b\in \mathrm{Fin}\left(n\right),\forall dG\in \mathrm{Real},\forall dP\in \mathrm{Real},(\mathrm{SimpleGraph}.\mathrm{Connected}\left(G\right))\Rightarrow ((a\ne b)\Rightarrow ((\mathrm{HasDerivAt}\left(\mathrm{fun}t:\mathrm{Real}\mapsto \mathrm{kemeny}\left(\mathrm{paramAdj}\left(G,a,b,t\right)\right),dG,0\right))\Rightarrow ((\mathrm{HasDerivAt}\left(\mathrm{fun}t:\mathrm{Real}\mapsto \mathrm{kemeny}\left(\mathrm{paramAdj}\left(\mathrm{SimpleGraph}.\mathrm{pathGraph}\left(n\right),⟨0⟩,⟨n-1⟩,t\right)\right),dP,0\right))\Rightarrow (dP\le dG))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.result (✓ std3). ∎

Resolves. Problems/albright-et-al-2023-kemeny-edge-derivative-conjecture-3-5 (refuted) by D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.result.

Source. Repository-derived.

Acknowledgement. C. Albright; K. P. Hadaway; A. H. Pomerance; J. Jeffries; K. J. Lorenzen; A. K. Nix (2023). On the Edge Derivative of the Normalized Laplacian with Applications to Kemeny’s Constant. DOI: 10.48550/arXiv.2211.01495. URL: https://arxiv.org/abs/2211.01495v2.

Commentary.

Take cliques on {0,…,7} and {8,…,15}, joined by the path 0,16,17,18,19,20,21,22,8. This is a connected simple graph on Fin 23. The missing chord {0,8} has Kemeny derivative −7683669/4096 at zero, while the missing chord {0,22} of pathGraph 23 has derivative −77763/44. The difference is −4891047/45056 < 0. Grounded Green matrices give exact inverse certificates; spectral diagonalization identifies their weighted trace with the sum over nonzero characteristic roots. A rational rank-one update holds on a neighborhood of zero and yields both derivatives. Thus the universal minimality statement fails. No infinite family or asymptotic minimum is asserted.

References

• Truth anchor: D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.claim
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.kemeny
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.normLap
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.paramAdj
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.reciprocalRoots
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.reciprocalRoots_eq_sum
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.reciprocalRoots_eq_trace
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/AlbrightKemenyEdgeDerivativeRefutation.result