An infinite twin-free theta separating family

Abstract

An infinite twin-free theta separating family.

Definition 1.1 (The infinite-family question).

$$\mathrm{claim}=\exists orders:\mathrm{Nat}\to \mathrm{Nat},\exists graphs:(i:\mathrm{Nat})\to \mathrm{SimpleGraph}\left(\mathrm{Fin}\left(orders\left(i\right)\right)\right),(\forall i:\mathrm{Nat},((graphs\left(i\right)).\mathrm{Connected})\wedge ((\mathrm{TwinFree}\left(graphs\left(i\right)\right))\wedge (((\mathrm{mmL}\left(graphs\left(i\right)\right)=\mathrm{metricDimension}\left(graphs\left(i\right)\right))\wedge (\mathrm{mmQ}\left(graphs\left(i\right)\right)\ne \mathrm{metricDimension}\left(graphs\left(i\right)\right)))\vee ((\mathrm{mmQ}\left(graphs\left(i\right)\right)=\mathrm{metricDimension}\left(graphs\left(i\right)\right))\wedge (\mathrm{mmL}\left(graphs\left(i\right)\right)\ne \mathrm{metricDimension}\left(graphs\left(i\right)\right))))))\wedge (\forall i:\mathrm{Nat},\forall j:\mathrm{Nat},(i\ne j)\Rightarrow (\neg (\mathrm{Nonempty}\left((graphs\left(i\right)).\mathrm{Iso}\left(graphs\left(j\right)\right)\right))))$$

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

Citation. Monther Rashed Alfuraidan, Suliman Khan, Lorenzo Sauras-Altuzarra (2026). Metric dimension and maximum eigenvalue multiplicity of graph Laplacians. DOI: 10.48550/arXiv.2610.26875. URL: https://arxiv.org/abs/2610.26875v1.

Commentary.

Problem 30 (p. 27): “Do there exist infinite families of connected twin-free graphs satisfying exactly one of the two equalities mm_L(G)=dim(G), mm_Q(G)=dim(G)? The computational census shows that finite twin-free examples occur in both directions.” The carrier of graph i is Fin (orders i). Pairwise nonisomorphism expresses infinitude; the disjunction allows either equality direction in each member.

Theorem 1.2 (An infinite separating family).

$$\exists orders:\mathrm{Nat}\to \mathrm{Nat},\exists graphs:(i:\mathrm{Nat})\to \mathrm{SimpleGraph}\left(\mathrm{Fin}\left(orders\left(i\right)\right)\right),(\forall i:\mathrm{Nat},((graphs\left(i\right)).\mathrm{Connected})\wedge ((\mathrm{TwinFree}\left(graphs\left(i\right)\right))\wedge (((\mathrm{mmL}\left(graphs\left(i\right)\right)=\mathrm{metricDimension}\left(graphs\left(i\right)\right))\wedge (\mathrm{mmQ}\left(graphs\left(i\right)\right)\ne \mathrm{metricDimension}\left(graphs\left(i\right)\right)))\vee ((\mathrm{mmQ}\left(graphs\left(i\right)\right)=\mathrm{metricDimension}\left(graphs\left(i\right)\right))\wedge (\mathrm{mmL}\left(graphs\left(i\right)\right)\ne \mathrm{metricDimension}\left(graphs\left(i\right)\right))))))\wedge (\forall i:\mathrm{Nat},\forall j:\mathrm{Nat},(i\ne j)\Rightarrow (\neg (\mathrm{Nonempty}\left((graphs\left(i\right)).\mathrm{Iso}\left(graphs\left(j\right)\right)\right))))$$

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

Resolves. Problems/aks2610 (proved) by D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaSeparation.result.

Source. Repository-derived.

Acknowledgement. Monther Rashed Alfuraidan, Suliman Khan, Lorenzo Sauras-Altuzarra (2026). Metric dimension and maximum eigenvalue multiplicity of graph Laplacians. DOI: 10.48550/arXiv.2610.26875. URL: https://arxiv.org/abs/2610.26875v1.

Commentary.

Take orders i=6(i+1)+9 and graphs i=thetaGraph (6(i+1)+4). Every graph is connected and twin-free, its metric dimension and Laplacian maximum multiplicity equal 2, and its signless maximum multiplicity is at most 1. Distinct orders exclude isomorphisms.

References

• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaSeparation.claim
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaSeparation.result
• Dependency: D5/S3/Combinatorics/Graph/SubgroupGenerating/CyclicExtensionRefutation
• Dependency: D5/S3/Combinatorics/SpectralGraph/BonettoSignature
• Dependency: D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaRecurrence
• Dependency: D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaStructure