The order-one boundary of the cyclic SGB extension

Abstract

The complete finite-cyclic extension of the Section 5 SGB assertions is false at order one.

Definition 1.1 (The two vertex parts).

$$\mathrm{Vertex}\left(G\right)=\mathrm{Sum}\left(\mathrm{Prod}\left(G,G\right),\mathrm{Subgroup}\left(G\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.Vertex (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

For a group G, the left summand contains every ordered pair of elements, including repetitions and the identity pair. The right summand contains every subgroup, including the trivial subgroup. Sum distinguishes the two parts even if their underlying sets overlap. No quotient or deletion is made.

Definition 1.2 (The source graph).

$$\begin{array}{r}\mathrm{Adj}\left(\mathrm{sgbGraph}\left(G\right),\mathrm{inl}\left(p\right),\mathrm{inr}\left(H\right)\right)\iff \mathrm{closure}\left(\left\{\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right\}\right)=H\\ \mathrm{Adj}\left(\mathrm{sgbGraph}\left(G\right),\mathrm{inr}\left(H\right),\mathrm{inl}\left(p\right)\right)\iff \mathrm{closure}\left(\left\{\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right\}\right)=H\\ \neg \mathrm{Adj}\left(\mathrm{sgbGraph}\left(G\right),\mathrm{inl}\left(p\right),\mathrm{inl}\left(q\right)\right)\\ \neg \mathrm{Adj}\left(\mathrm{sgbGraph}\left(G\right),\mathrm{inr}\left(H\right),\mathrm{inr}\left(J\right)\right)\end{array}$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.sgbGraph (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

Das–Erfanian–Nath define this graph in Section 1, and Section 2 uses disjoint union. For every pair p and subgroup H, the two cross-adjacency directions are exactly closure({p.1,p.2}) = H. The closure is the subgroup generated by the two entries. Both same-part adjacency relations are false. This gives a simple undirected graph directly on Vertex G, without a labelled cyclic representative or a divisors-only surrogate.

Definition 1.3 (All subgroups form a finite type).

$$\mathrm{hasType}\left(\mathrm{subgroupFintype}\left(G\right),\mathrm{Fintype}\left(\mathrm{Subgroup}\left(G\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.subgroupFintype (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

For a finite group G, the coercion taking a subgroup to its underlying subset is injective by SetLike.coe_injective. The finite type of subsets of G therefore supplies Fintype (Subgroup G) through Fintype.ofInjective. This local instance enumerates all subgroups, including bottom, and imposes no cyclicity or nontriviality assumption.

Definition 1.4 (The four matrix choices).

$$\mathrm{hasType}\left(MatrixKind,Type\right)$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.MatrixKind (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

The four constructor names select adjacency, Laplacian, signless Laplacian and common-neighbour matrices, respectively.

Definition 1.5 (Literal common-neighbour counts).

$$\mathrm{commonNeighbourMatrix}\left(g,i,j\right)=\{\begin{array}{rl}0& i=j\\ (\mathrm{card}\left(\{k\mid k\ne i\wedge \left(k\ne j\wedge \left(\mathrm{Adj}\left(g,i,k\right)\wedge \mathrm{Adj}\left(g,j,k\right)\right)\right)\}\right):\mathbb{R})& i\ne j\end{array}$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.commonNeighbourMatrix (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

For a finite vertex type V, CN has zero diagonal. At distinct i and j, its entry is the cardinality, cast to the reals, of the vertices k different from both i and j and adjacent to both. The displayed set ranges over all k in V. Thus CN is the source’s common-neighbour count matrix, rather than the zero-one common-neighbour graph.

Definition 1.6 (Adjacency, degree and the four matrices).

$$\begin{array}{r}\mathrm{sourceMatrix}\left(g,adjacency\right)=\mathrm{adjMatrix}\left(g,\mathbb{R}\right)\\ \mathrm{sourceMatrix}\left(g,laplacian\right)=\mathrm{degMatrix}\left(g,\mathbb{R}\right)-\mathrm{adjMatrix}\left(g,\mathbb{R}\right)\\ \mathrm{sourceMatrix}\left(g,signless\right)=\mathrm{degMatrix}\left(g,\mathbb{R}\right)+\mathrm{adjMatrix}\left(g,\mathbb{R}\right)\\ \mathrm{sourceMatrix}\left(g,commonNeighbour\right)=\mathrm{commonNeighbourMatrix}\left(g\right)\end{array}$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.sourceMatrix (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

A is Mathlib SimpleGraph.adjMatrix over the reals, with entry one on an edge and zero otherwise. D is SimpleGraph.degMatrix, the diagonal of the actual neighbour counts. L is SimpleGraph.lapMatrix = D-A; Q is D+A. The fourth choice is the literal commonNeighbourMatrix. All four matrices are Hermitian: the first three use the corresponding Mathlib symmetry results, and CN is symmetric by interchange of its two counted-neighbour conditions.

Theorem 1.7 (Each source matrix is Hermitian).

$$\forall V\in Type,[\mathrm{Fintype}\left(V\right)],\forall g\in \mathrm{SimpleGraph}\left(V\right),\forall kind\in MatrixKind,Matrix.IsHermitian\left(\mathrm{sourceMatrix}\left(g,kind\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.source_matrix_isHermitian (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

For every finite vertex type V, simple graph g and matrix choice kind, sourceMatrix g kind is Hermitian. The adjacency, Laplacian and degree matrices are real symmetric; interchanging the vertices preserves the common-neighbour count. The graphSpectrum definition uses this theorem to enumerate the real eigenvalues with multiplicities.

Definition 1.8 (Actual spectra with multiplicity).

$$\text{let}hM:\mathrm{IsHermitian}\left(\mathrm{sourceMatrix}\left(g,kind\right)\right),\mathrm{graphSpectrum}\left(g,kind\right)=\mathrm{map}\left(\mathrm{eigenvalues}\left(hM\right),\mathrm{univ}\left(V\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.graphSpectrum (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

Let M = sourceMatrix(g,kind), and let hM be its Hermitian proof. The multiset maps hM.eigenvalues over the entire finite index type V. The definition also applies RCLike.ofReal, which is the identity in the real field. Mathlib Matrix.IsHermitian.roots_charpoly_eq_eigenvalues identifies this multiset with M.charpoly.roots. Consequently algebraic multiplicity is retained and no integer-valued surrogate or selected subset of eigenvalues is used.

Definition 1.9 (Integer eigenvalues).

$$\mathrm{IntegralSpectrum}\left(s\right)\iff \left(\forall x\in \mathbb{R},x\in s\Rightarrow \left(\exists z\in \mathbb{Z},x=(z:\mathbb{R})\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.IntegralSpectrum (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

Integral means that every member of the actual real eigenvalue multiset equals the real image of some integer. Integer matrix entries or integer characteristic coefficients alone would not satisfy this definition.

Definition 1.10 (The whole-graph center).

$$\mathrm{averageDegree}\left(g\right)=\frac{2\cdot (\mathrm{card}\left(\mathrm{edgeFinset}\left(g\right)\right):\mathbb{R})}{(\mathrm{card}\left(V\right):\mathbb{R})}$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.averageDegree (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

The center is twice the number of actual unordered edges divided by the total number of vertices. Both counts belong to the entire graph, including every component and every subgroup vertex. There is no separate component centering.

Definition 1.11 (The four absolute energies).

$$\begin{array}{r}\mathrm{graphEnergy}\left(g,kind\right)=\sum _{x\in \mathrm{graphSpectrum}\left(g,kind\right)}\left|x-\mathrm{center}\left(g,kind\right)\right|\\ \mathrm{center}\left(g,laplacian\right)=\mathrm{averageDegree}\left(g\right)\\ \mathrm{center}\left(g,signless\right)=\mathrm{averageDegree}\left(g\right)\\ \mathrm{center}\left(g,adjacency\right)=0\\ \mathrm{center}\left(g,commonNeighbour\right)=0\end{array}$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.graphEnergy (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

The sum is a multiset sum, so repeated eigenvalues contribute repeatedly. For adjacency and CN, center is zero. For Laplacian and signless Laplacian, center is averageDegree(g), exactly the whole-graph 2m/N used in Section 5. The construction applies equally to the SGB graph and each complete-graph benchmark.

Definition 1.12 (The complete ten-clause list).

$$\mathrm{sourceBundle}\left(g\right)\iff \left(\left(\neg \mathrm{IntegralSpectrum}\left(\mathrm{graphSpectrum}\left(g,adjacency\right)\right)\right)\wedge \left(\mathrm{IntegralSpectrum}\left(\mathrm{graphSpectrum}\left(g,laplacian\right)\right)\wedge \left(\mathrm{IntegralSpectrum}\left(\mathrm{graphSpectrum}\left(g,signless\right)\right)\wedge \left(\mathrm{IntegralSpectrum}\left(\mathrm{graphSpectrum}\left(g,commonNeighbour\right)\right)\wedge \left(\mathrm{graphEnergy}\left(g,adjacency\right)<(\mathrm{card}\left(V\right):\mathbb{R})\wedge \left(\mathrm{graphEnergy}\left(g,adjacency\right)\le \mathrm{graphEnergy}\left(K\left(V\right),adjacency\right)\wedge \left(\mathrm{graphEnergy}\left(g,laplacian\right)\le \mathrm{graphEnergy}\left(K\left(V\right),laplacian\right)\wedge \left(\mathrm{graphEnergy}\left(g,signless\right)\le \mathrm{graphEnergy}\left(K\left(V\right),signless\right)\wedge \left(\mathrm{graphEnergy}\left(g,commonNeighbour\right)\le \mathrm{graphEnergy}\left(K\left(V\right),commonNeighbour\right)\wedge \mathrm{graphEnergy}\left(g,adjacency\right)\le \mathrm{graphEnergy}\left(g,laplacian\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.sourceBundle (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

The displayed conjunction preserves every clause of the closing (a)-(c) list: adjacency nonintegrality; L, Q and CN integrality; strict E < card(V); four separate non-hyperenergeticity bounds; and E <= LE. In the four benchmark clauses, K(V) denotes the actual complete SimpleGraph on the same type V, namely top. Its respective energy is evaluated by the same graphEnergy definition. This is the same-order complete graph in the original definitions; no benchmark estimate is substituted.

Definition 1.13 (The unrestricted finite-cyclic extension).

$$claim\iff \left(\forall G\in Type,[\mathrm{Group}\left(G\right)],[\mathrm{Fintype}\left(G\right)],[\mathrm{IsCyclic}\left(G\right)],\mathrm{sourceBundle}\left(\mathrm{sgbGraph}\left(G\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.claim (✓ std3).

Citation. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

The source’s closing invitation follows its complete (a)-(c) summary for the known orders p^n, pq, p^2q and p^2q^2, with distinct primes and n >= 1. Those families are results of Das–Erfanian–Nath. The ambient framework is finite groups. Group supplies nonemptiness, Fintype supplies finiteness and IsCyclic supplies cyclicity, so every positive finite order, including one, is retained. The finite-subgroup enumeration is obtained injectively from subsets of G. Decidable choices used to form finite matrices impose no extra group restriction. The invitation is unlabelled; no numbered conjecture or private author-intent assertion is introduced.

Theorem 1.14 (The whole extension is false).

$$\neg claim$$

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

Resolves. Problems/das-2026-whole-cyclic-sgb-extension-refutation (refuted) by D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.result.

Source. Repository-derived.

Acknowledgement. Shrabani Das; Ahmad Erfanian; Rajat Kanti Nath (2026). Certain topological indices and spectral properties of SGB-graphs of finite cyclic groups. DOI: 10.48550/arXiv.2602.07587. URL: https://arxiv.org/abs/2602.07587v1.

Commentary.

Use the order-one group PUnit with its existing cyclic-group instance. The complete typed vertex union has one pair vertex and one subgroup vertex. An explicit equivalence to Fin 2 has both inverse laws proved. Reindexing the actual adjacency matrix gives [[0,1],[1,0]], whose characteristic polynomial is (X-1)(X+1). Matrix.charpoly_reindex preserves that polynomial, and the Hermitian characteristic-root theorem gives the actual eigenvalue multiset {1,-1}. Both eigenvalues are integers, contradicting the first conjunct when the entire universal is specialized to this group. The other nine conjuncts remain in claim. This refutes the unrestricted finite extension; it makes no claim against a variant excluding order one or against the known source families.

References

• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.IntegralSpectrum
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.MatrixKind
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.Vertex
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.averageDegree
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.claim
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.commonNeighbourMatrix
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.graphEnergy
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.graphSpectrum
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.result
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.sgbGraph
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.sourceBundle
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.sourceMatrix
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.source_matrix_isHermitian
• Truth anchor: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation.subgroupFintype