An infinite twin-free theta family separating the Laplacian equalities

Alfuraidan, Khan and Sauras-Altuzarra, Metric dimension and maximum eigenvalue multiplicity of graph Laplacians, arXiv:2610.26875v1, Problem 30, p. 27, ask:

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 result answers this existence question affirmatively. Here $\dim(G)$ is the minimum size of a resolving set for actual shortest-path distances, $\operatorname{mm}_L$ and $\operatorname{mm}_Q$ maximize real eigenspace dimension over every real eigenvalue, and twin-freeness excludes both true and false twins. The signless Laplacian is $D(G)+A(G)$.

Statement echo

| Source clause | Formal counterpart | | --- | --- | | Finite simple graphs | SimpleGraph (Fin (orders i)) in claim | | Connected | the connectivity conjunct for every natural index | | Twin-free, both kinds | TwinFree, defined using neighborhoods with the other vertex removed | | Metric dimension | minimum cardinality of an injective distance representation | | Maximum multiplicity | maximumMultiplicity, using actual real eigenspaces and all real eigenvalues | | Exactly one equality | disjunction of one equality and the other inequality | | Infinite family | all-natural indexing and pairwise nonisomorphism |

The concrete witness has $G_i=\Theta_{3,3,6(i+1)+4}$ and order $6(i+1)+9$. The source permits either equality direction; the construction uniformly supplies the Laplacian direction. No source clause is dropped. The fixed finite carrier only labels the graph; pairwise nonisomorphism expresses infinitude independently of labels.

The source's finite examples do not establish an infinite family. The settling declaration is TwinFreeThetaSeparation.result, under open-problem-resolution (#22167; Proved). The two supporting modules use escape-witness: graph connectivity and exact metric certificates in TwinFreeThetaStructure, and the continuant obstruction and coordinate dimension bounds in TwinFreeThetaRecurrence.

The conclusion is existence in one equality direction. An infinite family in the opposite direction, a full classification for Problem 29, and the exact signless maximum multiplicity for every family member remain open in this delivery. Literature completeness is ASSUMED-UNVERIFIED.

The graph consists of three internally disjoint paths sharing their two terminals, of lengths $3,3,r$. Exact distance formulas give a two-landmark resolving set, and a lower-bound argument excludes a single landmark. The neighborhood identities give the actual Laplacian and signless vertex equations. Their solutions map injectively into the coordinate model.

Away from $t=1,-1$, the continuant collision exclusion bounds the coordinate dimension by one. The singular terminal systems bound the Laplacian case by two and the signless case by one. For $r=6k+4$, an injective linear map from $\mathbb R^2$ supplies Laplacian eigenvectors at eigenvalue $1$. Together these give $\operatorname{mm}_L=2$ and $\operatorname{mm}_Q\le1$. Distinct orders exclude graph isomorphisms. These are statements about actual eigenspaces, without a numerical spectral surrogate.

A failure of connectivity, twin exclusion, metric dimension two, the Laplacian multiplicity equality, the signless upper bound, or pairwise nonisomorphism in the specified all-natural family would refute the formal construction. A finite census alone cannot establish its universal quantifier.

The settlement is D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaSeparation.result. Its Scribe associates exactly one OpenProblemResolutionClaim(Proved) with this dossier. Supporting and private declarations named below provide the corresponding kernel-checked statements; explanatory prose is not an additional Lean theorem.

The escape audit is unfinished for all six authored public theorems: TwinFreeThetaStructure.theta_adj, theta_metric_certificates, TwinFreeThetaRecurrence.model_nonsingular_finrank, model_laplacian_singular_finrank, model_signless_singular_finrank, and TwinFreeThetaSeparation.result. The missing typed reconstruction and variation/dependence evidence is recorded in issue #23310. No four-slot registration is claimed validated.

Exact finite checker

Published experiment directory. The program is check.py, SHA-256 7be8ba1d9172ee551a0c80f47ecd42e7b7215f212df2345d7de92b9c3186dfbc. Command: python3 /tmp/op-aks2610/check.py, using the byte-identical script extracted from that immutable revision; exit 0, ALL_CHECKS_OK. The family checks cover $k=1,\ldots,8$, and the continuant identities cover indices $1,\ldots,80$. They compute twin exclusion, metric dimension two, $\operatorname{mm}_L=2$ and $\operatorname{mm}_Q=1$ in that finite range. These computations do not prove the all-natural result.

| Item | Status and evidence | | --- | --- | | Metric and twin statements for every $r\ge10$; spectral restriction $r=6k+4$, $k\ge1$ | Kernel-checked: private TwinFreeThetaStructure.theta_metric_dimension, theta_twin_free; spectral range in TwinFreeThetaSeparation.theta_maximum_multiplicities. | | Exact vertex equations, nonsingular collision exclusion, separate $t=1,-1$ systems, two independent real parameters at Laplacian eigenvalue $1$ | Kernel-checked: eigen_neighbor_equation, graphCoordinates, TwinFreeThetaRecurrence.quadratic_collision_excluded, singular_boundary_systems, TwinFreeThetaSeparation.thetaLift_eigen, thetaLift_injective. | | Abstract recurrence and coordinate-model bounds | Kernel-checked: TwinFreeThetaRecurrence.model_nonsingular_finrank, model_laplacian_singular_finrank, model_signless_singular_finrank. | | Connectivity, both twin exclusions and metric dimension two for the exact theta family | Kernel-checked: TwinFreeThetaStructure.theta_metric_certificates; the twin predicate covers both adjacency cases. | | Exact neighborhood/matrix equations and realization on actual eigenspaces | Kernel-checked: private TwinFreeThetaSeparation.theta_operator_row, eigen_neighbor_equation, graphCoordinates, graph_coordinates_exist. | | Infinite-family existence using $\operatorname{mm}_L=2$, $\operatorname{mm}_Q\le1$ | Kernel-checked: TwinFreeThetaSeparation.result and private theta_maximum_multiplicities. | | Supplied checker | Computed: published checker, exit 0, ALL_CHECKS_OK, exact scope above. | | Broader independent graph/eigenvector checks | Open (ASSUMED-UNVERIFIED): the target reports graph checks at $r=10,\ldots,100$ and eigenvector checks at $k=1,\ldots,30$, but no matching program at the cited experiment revision supplies those ranges. This differs from the target's computed label because published matching program evidence is missing. | | Opposite direction, complete Problem 29 classification, exact uniform $\operatorname{mm}_Q=1$ | Open: no such theorem is asserted in this delivery; the uniform kernel-checked conclusion needed here is $\operatorname{mm}_Q\le1$. |

What the settlement shows

The decisive mechanism is that exchanging whole paths permits a Laplacian eigenspace of dimension two without creating vertex twins, while the signless terminal systems and nonsingular obstruction bound every signless eigenspace dimension by one. The metric and twin statements extend to every $r\ge10$; the spectral separation is proved for $r=6k+4$, $k\ge1$. The argument settles the source's existence question in the Laplacian equality direction. It supplies no reverse-direction family, no complete theta classification, and no change to a separately stated source theorem is claimed.

The literature screen in #22167 inspected the source version, repository and selected third-party/library results and title/citation queries. Some citation endpoints were rate-limited; complete citation enumeration, worldwide openness, priority and originality are not certified. The source-to-formal correspondence is a content assessment, distinct from the Lean kernel's verification. The broader independent finite checks listed in Triage lack published matching program evidence here. The four-slot escape audit remains unfinished under #23310.