Distance Seidel energy after deleting an edge

Abstract

Deleting any edge of a complete bipartite graph with both parts of size at least two strictly increases its distance Seidel energy for the matrix J - I - 2D.

Definition 1.1 (Distance Seidel matrix).

$$\forall (V:Type),[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall (G:\mathrm{SimpleGraph}\left(V\right)),\mathrm{distSeidel}\left(G\right)=Matrix.of\left(\mathrm{fun}(u:V)\mapsto \mathrm{fun}(v:V)\mapsto 1-\mathrm{ite}\left((u=v),1,0\right)-2\cdot (SimpleGraph.dist\left(G,u,v\right):\mathbb{R})\right)$$

Formalization. D5/S3/Combinatorics/Graph/KyFanGap/HarithaChithraDistanceSeidelEnergy.distSeidel (✓ std3).

Citation. T. Haritha and A. V. Chithra (2022). Distance Seidel matrix of a connected graph. DOI: 10.1080/09728600.2025.2479147. URL: https://arxiv.org/abs/2210.05940v2.

Commentary.

Page 2: “D^S(G) = J − I − 2D = −1 if v_r is adjacent to v_t, 1 − 2d_G(v_r, v_t) otherwise.” The displayed expression encodes J − I − 2D entrywise using SimpleGraph.dist, with zero diagonal. The source’s casewise expression instead gives diagonal one. Only the matrix equation is used here. On the complete bipartite graphs and their single-edge deletions considered below, every pair is connected.

Definition 1.2 (Problem 5.1).

$$\mathrm{claim}=(\forall (a:\mathbb{N}),\forall (b:\mathbb{N}),(2\le a)\Rightarrow ((2\le b)\Rightarrow (\forall (e:Sym2\left(\mathrm{Sum}\left(\mathrm{Fin}\left(a\right),\mathrm{Fin}\left(b\right)\right)\right)),(e\in SimpleGraph.edgeSet\left(\mathrm{completeBipartiteGraph}\left(\mathrm{Fin}\left(a\right),\mathrm{Fin}\left(b\right)\right)\right))\Rightarrow (\mathrm{energy}\left(\mathrm{distSeidel}\left(\mathrm{completeBipartiteGraph}\left(\mathrm{Fin}\left(a\right),\mathrm{Fin}\left(b\right)\right)\right)\right)<\mathrm{energy}\left(\mathrm{distSeidel}\left(SimpleGraph.deleteEdges\left(\mathrm{completeBipartiteGraph}\left(\mathrm{Fin}\left(a\right),\mathrm{Fin}\left(b\right)\right),\{e\}\right)\right)\right)))))$$

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

Citation. T. Haritha and A. V. Chithra (2022). Distance Seidel matrix of a connected graph. DOI: 10.1080/09728600.2025.2479147. URL: https://arxiv.org/abs/2210.05940v2.

Commentary.

Problem 5.1, page 13: “Let G = K_{a,b}, with a, b > 1. Is E_{D^S}(K_{a,b} − e) > E_{D^S}(K_{a,b}), for any edge e of K_{a,b}?” The proposition gives the affirmative universal statement. The vertex type is Fin a ⊕ Fin b; edges are unordered pairs in the edge set. The natural-number inequalities 2 ≤ a and 2 ≤ b express a, b > 1. SimpleGraph.deleteEdges removes the singleton edge set.

Theorem 1.3 (Strict increase for every edge).

$$\forall (a:\mathbb{N}),\forall (b:\mathbb{N}),(2\le a)\Rightarrow ((2\le b)\Rightarrow (\forall (e:Sym2\left(\mathrm{Sum}\left(\mathrm{Fin}\left(a\right),\mathrm{Fin}\left(b\right)\right)\right)),(e\in SimpleGraph.edgeSet\left(\mathrm{completeBipartiteGraph}\left(\mathrm{Fin}\left(a\right),\mathrm{Fin}\left(b\right)\right)\right))\Rightarrow (\mathrm{energy}\left(\mathrm{distSeidel}\left(\mathrm{completeBipartiteGraph}\left(\mathrm{Fin}\left(a\right),\mathrm{Fin}\left(b\right)\right)\right)\right)<\mathrm{energy}\left(\mathrm{distSeidel}\left(SimpleGraph.deleteEdges\left(\mathrm{completeBipartiteGraph}\left(\mathrm{Fin}\left(a\right),\mathrm{Fin}\left(b\right)\right),\{e\}\right)\right)\right))))$$

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

Resolves. Problems/haritha-chithra-2022-distance-seidel-energy-problem-5-1 (proved) by D5/S3/Combinatorics/Graph/KyFanGap/HarithaChithraDistanceSeidelEnergy.result.

Source. Repository-derived.

Acknowledgement. T. Haritha and A. V. Chithra (2022). Distance Seidel matrix of a connected graph. DOI: 10.1080/09728600.2025.2479147. URL: https://arxiv.org/abs/2210.05940v2.

Commentary.

The distance Seidel matrix of the complete bipartite graph has energy 6(a+b−2). Its sign is a symmetric involution which reflects the two part-indicator directions. Deleting an edge changes only the two corresponding off-diagonal entries, each by −4. This preserves the supporting trace functional. Equality in the trace bound for the sum of absolute eigenvalues would force commutation with the involution, whereas a commutator entry is 8/a at another vertex of the first part. Since a ≥ 2, that entry is nonzero and the energy inequality is strict. The proof treats every a,b ≥ 2, including the cases a = 2 and a = 3 of Propositions 5.2–5.3. It makes no universal assertion about the alternative diagonal-one matrix.

References

• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/HarithaChithraDistanceSeidelEnergy.claim
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/HarithaChithraDistanceSeidelEnergy.distSeidel
• Truth anchor: D5/S3/Combinatorics/Graph/KyFanGap/HarithaChithraDistanceSeidelEnergy.result
• Dependency: D5/S3/Combinatorics/Graph/KyFanGap/MandalMehatariDasSeidelMinimum