Minimum Seidel energy of chain graphs

Abstract

Every connected chain graph has at least the Seidel energy of each member of Gamma(n,k), with equality precisely for the members of that family.

Definition 1.1 (Characteristic-root energy).

$$\forall (V:Type),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall (M:\mathrm{Matrix}\left(V,V,\mathbb{R}\right)),\mathrm{energy}\left(M\right)=Multiset.sum\left(Multiset.map\left(\mathrm{fun}(x:\mathbb{R})\mapsto |x|,Polynomial.roots\left(Matrix.charpoly\left(M\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.energy (✓ std3).

Citation. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

Page 2: “The Seidel energy SE(G) of a graph G is defined as the sum of absolute values of the eigenvalues of Seidel matrix S.” The expression uses real characteristic roots with multiplicity. Its applications here are real symmetric matrices.

Theorem 1.2 (Energy in an eigenbasis).

$$\forall (V:Type),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall (X:\mathrm{Matrix}\left(V,V,\mathbb{R}\right)),\forall (hX:Matrix.IsHermitian\left(X\right)),\mathrm{energy}\left(X\right)=Finset.sum\left(Finset.univ,\mathrm{fun}(i:V)\mapsto |Matrix.IsHermitian.eigenvalues\left(hX,i\right)|\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.energy_eigenvalues (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

For a real symmetric matrix, the real roots of the characteristic polynomial are precisely its eigenvalues with multiplicity.

Theorem 1.3 (Trace of the positive square root).

$$\forall (V:Type),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall (X:\mathrm{Matrix}\left(V,V,\mathbb{R}\right)),\forall (hX:Matrix.IsHermitian\left(X\right)),Finset.sum\left(Finset.univ,\mathrm{fun}(i:V)\mapsto |Matrix.IsHermitian.eigenvalues\left(hX,i\right)|\right)=Matrix.trace\left(CFC.sqrt\left(Matrix.transpose\left(X\right)\cdot X\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.sum_abs_eq_trace_sqrt (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

The positive square root of the transpose product has absolute eigenvalues. Its trace is their sum.

Theorem 1.4 (Occurrences in an indexed list).

$$\forall (alpha:Type),[\mathrm{DecidableEq}\left(alpha\right)]\forall (n:\mathbb{N}),\forall (f:\mathrm{Fin}\left(n\right)\to alpha),\forall (p:alpha),List.count\left(p,List.ofFn\left(f\right)\right)=Finset.sum\left(Finset.univ,\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{ite}\left(f\left(i\right)=p,1,0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.count_ofFn (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

Counting a letter in a finite indexed list equals summing its equality indicators.

Definition 1.5 (The alternating binary string).

$$\forall (k:\mathbb{N}),\forall (s:\mathrm{Fin}\left(k\right)\to \mathbb{N}),\forall (t:\mathrm{Fin}\left(k\right)\to \mathbb{N}),\mathrm{binaryString}\left(s,t\right)=List.flatten\left(List.ofFn\left(\mathrm{fun}(i:\mathrm{Fin}\left(k\right))\mapsto List.append\left(List.replicate\left(s\left(i\right),Bool.false\right),List.replicate\left(t\left(i\right),Bool.true\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.binaryString (✓ std3).

Citation. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

Page 2, verbatim: We represent a chain graph $G$ on $n$ vertices using a binary string $b={\alpha }_1{\alpha }_2{\alpha }_3\dots {\alpha }_n$ of length $n$, where ${\alpha }_i=0$ if the vertex $v_i$ is added as an isolated vertex, and ${\alpha }_i=1$ if the vertex $v_i$ is dominating to all the previously added isolated vertices. As we start from a single vertex we always take ${\alpha }_1=0$, and since we are considering connected graphs only so ${\alpha }_n=1$. For any $n$ vertex chain graph, without loss of generality, we represent it by the binary string $b=0^{s_1}{1}^{t_1}{0}^{s_2}\dots 0^{s_k}{1}^{t_k}$, where $s_i,t_i\ge 1$ and ${\sum }_{i=1}^k(s_i+t_i)=n$. A chain graph is a bipartite graph, and it is complete bipartite if and only if $k=1$.

The indices are Fin k; false is 0 and true is 1. List.ofFn orders the runs and List.flatten concatenates them.

Definition 1.6 (The chain graph of a binary string).

$$\forall (b:\mathrm{List}\left(\mathrm{Bool}\right)),\forall (i:\mathrm{Fin}\left(List.length\left(b\right)\right)),\forall (j:\mathrm{Fin}\left(List.length\left(b\right)\right)),(SimpleGraph.Adj\left(\mathrm{chainGraph}\left(b\right),i,j\right))\iff (((i<j)\wedge ((List.get\left(b,i\right)=Bool.false)\wedge (List.get\left(b,j\right)=Bool.true)))\vee ((j<i)\wedge ((List.get\left(b,j\right)=Bool.false)\wedge (List.get\left(b,i\right)=Bool.true))))$$

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.chainGraph (✓ std3).

Citation. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

Page 2, verbatim: “adding an isolated vertex.” “adding a vertex dominating to all previously added isolated vertices only.” An earlier false position and a later true position are adjacent. The formula gives the entire adjacency relation, including its symmetric case and the absence of loops.

Definition 1.7 (The Seidel matrix).

$$\forall (n:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),\mathrm{seidel}\left(G\right)=Matrix.of\left(Function.const\left(\mathrm{Fin}\left(n\right),Function.const\left(\mathrm{Fin}\left(n\right),1:\mathbb{R}\right)\right)\right)-1-HSMul.hSMul\left(2:\mathbb{R},SimpleGraph.adjMatrix\left(G,\mathbb{R}\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.seidel (✓ std3).

Citation. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

Page 2, verbatim: Let $G$ be a simple, connected, finite graph with vertex set $V=\{v_1,v_2,\dots ,v_n\}$. Let $A$ be the (0,1)-adjacency matrix [12, 17] of $G$. Then the Seidel matrix [1, 2, 6, 9, 19, 20, 22, 23, 25] is a square matrix of order $n$ defined by $S=J-I-2\cdot A$, where $J$ is all $1$ matrix and $I$ is the identity matrix.

Here A is SimpleGraph.adjMatrix over the real numbers. The expression retains the all-ones matrix, identity matrix, and scalar multiple separately.

Definition 1.8 (The comparison family).

$$\forall (n:\mathbb{N}),\forall (k:\mathbb{N}),\forall (b:\mathrm{List}\left(\mathrm{Bool}\right)),\mathrm{Gamma}\left(n,k,b\right)=(\exists (s:\mathbb{N}),\exists (t:\mathbb{N}),(1\le s)\wedge ((s\le n-2\cdot k+1)\wedge ((1\le t)\wedge ((t\le n-2\cdot k+1)\wedge ((s+t=n-2\cdot k+2)\wedge (b=List.append\left(List.append\left(List.replicate\left(s,Bool.false\right),List.flatten\left(List.replicate\left(k-1,[Bool.true,Bool.false]\right)\right)\right),List.replicate\left(t,Bool.true\right)\right)))))))$$

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.Gamma (✓ std3).

Citation. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

Page 21: Let ${\Gamma }_{n,k}$ be a class of chain graphs of order $n$ with the binary string $b=0^{s_1}{1}^1{0}^1{1}^1{0}^1\dots 0^1{1}^{t_k}$ such that $s_1+t_k=n-2\cdot k+2$ with $1\le s_1\le n-2\cdot k+1$ and $1\le t_k\le n-2\cdot k+1$.

The middle word is k-1 copies of [true,false], representing the 2k-2 singleton runs under the source’s underbrace. Natural subtraction is truncated; every parameter is a natural number.

Definition 1.9 (Conjecture 4.14).

$$\mathrm{claim}=(\forall (n:\mathbb{N}),\forall (k:\mathbb{N}),(1\le k)\Rightarrow ((2\cdot k\le n)\Rightarrow (\forall (s:\mathrm{Fin}\left(k\right)\to \mathbb{N}),\forall (t:\mathrm{Fin}\left(k\right)\to \mathbb{N}),(\forall (i:\mathrm{Fin}\left(k\right)),1\le s\left(i\right))\Rightarrow ((\forall (i:\mathrm{Fin}\left(k\right)),1\le t\left(i\right))\Rightarrow ((Finset.sum\left(Finset.univ,\mathrm{fun}(i:\mathrm{Fin}\left(k\right))\mapsto s\left(i\right)+t\left(i\right)\right)=n)\Rightarrow (\forall (h:\mathrm{List}\left(\mathrm{Bool}\right)),(\mathrm{Gamma}\left(n,k,h\right))\Rightarrow ((\mathrm{energy}\left(\mathrm{seidel}\left(\mathrm{chainGraph}\left(h\right)\right)\right)\le \mathrm{energy}\left(\mathrm{seidel}\left(\mathrm{chainGraph}\left(\mathrm{binaryString}\left(s,t\right)\right)\right)\right))\wedge ((\mathrm{energy}\left(\mathrm{seidel}\left(\mathrm{chainGraph}\left(\mathrm{binaryString}\left(s,t\right)\right)\right)\right)=\mathrm{energy}\left(\mathrm{seidel}\left(\mathrm{chainGraph}\left(h\right)\right)\right))\iff (\mathrm{Gamma}\left(n,k,\mathrm{binaryString}\left(s,t\right)\right))))))))))$$

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.claim (✓ std3).

Citation. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

Conjecture 4.14, page 25, verbatim: Let $G$ be a chain graph of order $n$ with the binary string $b=0^{s_1}{1}^{t_1}{0}^{s_2}\dots 0^{s_k}{1}^{t_k}$ such that ${\sum }_{i=1}^k(s_i+t_i)=n,s_i\ge 1(1\le i\le k)$, and $t_i\ge 1(1\le i\le k)$. Then $\mathrm{SE}\left(G\right)\ge \mathrm{SE}\left(H\right)$, where $H\in {\Gamma }_{n,k}$. Moreover, the equality holds if and only if $G\in {\Gamma }_{n,k}$.

The functions s,t have domain Fin k and positive natural values; n is their total. Every comparison binary string h in Gamma n k is quantified separately. The energy is the shared characteristic-root energy of the real Seidel matrix.

Theorem 1.10 (Minimum energy and every equality case).

$$\forall (n:\mathbb{N}),\forall (k:\mathbb{N}),(1\le k)\Rightarrow ((2\cdot k\le n)\Rightarrow (\forall (s:\mathrm{Fin}\left(k\right)\to \mathbb{N}),\forall (t:\mathrm{Fin}\left(k\right)\to \mathbb{N}),(\forall (i:\mathrm{Fin}\left(k\right)),1\le s\left(i\right))\Rightarrow ((\forall (i:\mathrm{Fin}\left(k\right)),1\le t\left(i\right))\Rightarrow ((Finset.sum\left(Finset.univ,\mathrm{fun}(i:\mathrm{Fin}\left(k\right))\mapsto s\left(i\right)+t\left(i\right)\right)=n)\Rightarrow (\forall (h:\mathrm{List}\left(\mathrm{Bool}\right)),(\mathrm{Gamma}\left(n,k,h\right))\Rightarrow ((\mathrm{energy}\left(\mathrm{seidel}\left(\mathrm{chainGraph}\left(h\right)\right)\right)\le \mathrm{energy}\left(\mathrm{seidel}\left(\mathrm{chainGraph}\left(\mathrm{binaryString}\left(s,t\right)\right)\right)\right))\wedge ((\mathrm{energy}\left(\mathrm{seidel}\left(\mathrm{chainGraph}\left(\mathrm{binaryString}\left(s,t\right)\right)\right)\right)=\mathrm{energy}\left(\mathrm{seidel}\left(\mathrm{chainGraph}\left(h\right)\right)\right))\iff (\mathrm{Gamma}\left(n,k,\mathrm{binaryString}\left(s,t\right)\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.result (✓ std3). ∎

Resolves. Problems/mmd2205-seidelchain (proved) by D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.result.

Source. Repository-derived.

Acknowledgement. Santanu Mandal, Ranjit Mehatari, and Kinkar Chandra Das (2022). On the spectrum and energy of Seidel matrix for chain graphs. DOI: 10.48550/arXiv.2205.00310. URL: https://arxiv.org/abs/2205.00310v1.

Commentary.

Sign switching merges the first 0-run with the final 1-run. Compression gives a real symmetric odd core with weights at least one and first weight greater than one. Its trace-norm minimum and the constant inertia correction give the energy comparison. Equality forces every intermediate run to have length one, exactly the family Gamma. When k=1, switching a bipartition gives the all-ones matrix minus the identity for every graph in the comparison.

References

• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.Gamma
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.binaryString
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.chainGraph
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.claim
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.count_ofFn
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.energy
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.energy_eigenvalues
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.result
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.seidel
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum.sum_abs_eq_trace_sqrt
• Dependency: D5/S3/Observer/Hankel/BalancedHankelSchmidt
• Dependency: D5/S3/Weil/ZetaLinear/FullRankInertiaPullback