The token-graph cut bound fails on a five-cycle blow-up

Abstract

A phase product on the 100-token graph of the five-cycle blow-up with block size 40 has Rayleigh quotient below the cut and matching bound of Apte, Parekh and Sud.

Definition 1.1 (An unordered edge crossing a cut).

$$\forall (n:\mathbb{N}),\forall (S:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)),\forall (e:Sym2\left(\mathrm{Fin}\left(n\right)\right)),(\mathrm{crosses}\left(S,e\right))\iff (Sym2.\mathrm{lift}\left(⟨fun(u:\mathrm{Fin}\left(n\right))\mapsto fun(v:\mathrm{Fin}\left(n\right))\mapsto (u\in S)\ne (v\in S)⟩,e\right))$$

Formalization. D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.crosses (✓ std3).

Citation. Anuj Apte; Ojas Parekh; James Sud (2025). Conjectured Bounds for 2-Local Hamiltonians via Token Graphs. URL: https://arxiv.org/abs/2506.03441v2.

Commentary.

Page 8: “Let δ(S) be the set of edges in G that cross from S to V ∖ S, and Cut(S) be the sum of the weights of the edges δ(S).” Exactly one endpoint belongs to S. Sym2.lift descends the displayed symmetric endpoint predicate to unordered pairs; its proof of symmetry is implicit.

Definition 1.2 (The maximum cut).

$$\forall (n:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)],\mathrm{maxCut}\left(G\right)=\mathrm{Finset}.\sup \left((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right)\right)),fun(S:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right))\mapsto \mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left(fun(e:Sym2\left(\mathrm{Fin}\left(n\right)\right))\mapsto \mathrm{crosses}\left(S,e\right),\mathrm{SimpleGraph}.\mathrm{edgeFinset}\left(G\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.maxCut (✓ std3).

Citation. Anuj Apte; Ojas Parekh; James Sud (2025). Conjectured Bounds for 2-Local Hamiltonians via Token Graphs. URL: https://arxiv.org/abs/2506.03441v2.

Commentary.

Page 8: “We denote the maximum of Cut(S) over all S by C(G), i.e., C(G) is the solution to the Maximum Cut (MaxCut) problem on G.” Every edge has weight one, so the weight of a cut is the cardinality of the filtered unordered edge set. Finset.sup over all finite subsets gives the maximum, including the empty cut.

Definition 1.3 (The size-restricted maximum matching).

$$\forall (n:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)],\forall (k:\mathbb{N}),\mathrm{maxMatchingLe}\left(G,k\right)=\mathrm{Finset}.\sup \left(\mathrm{Finset}.\mathrm{filter}\left(fun(M:\mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right))\mapsto (\mathrm{Finset}.\mathrm{card}\left(M\right)\le k)\wedge (\mathrm{Set}.\mathrm{Pairwise}\left((M:\mathrm{Set}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right)),fun(e:Sym2\left(\mathrm{Fin}\left(n\right)\right))\mapsto fun(f:Sym2\left(\mathrm{Fin}\left(n\right)\right))\mapsto \mathrm{Disjoint}\left((e:\mathrm{Set}\left(\mathrm{Fin}\left(n\right)\right)),(f:\mathrm{Set}\left(\mathrm{Fin}\left(n\right)\right))\right)\right)),\mathrm{Finset}.\mathrm{powerset}\left(\mathrm{SimpleGraph}.\mathrm{edgeFinset}\left(G\right)\right)\right),fun(M:\mathrm{Finset}\left(Sym2\left(\mathrm{Fin}\left(n\right)\right)\right))\mapsto \mathrm{Finset}.\mathrm{card}\left(M\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.maxMatchingLe (✓ std3).

Citation. Anuj Apte; Ojas Parekh; James Sud (2025). Conjectured Bounds for 2-Local Hamiltonians via Token Graphs. URL: https://arxiv.org/abs/2506.03441v2.

Commentary.

Page 8: “Let M_k(G) denote the maximum weight matching under the restriction that |M| ≤ k.” For unit weights, weight is cardinality. The powerset ranges over edge subsets; Pairwise requires disjoint endpoint sets for distinct edges, and the cardinality is at most k. The coercion from an unordered edge to its endpoint set and that from a finite edge family to a set are shown explicitly.

Definition 1.4 (The least real adjacency eigenvalue).

$$\forall (iota:Type),[\mathrm{Fintype}\left(iota\right)],[\mathrm{DecidableEq}\left(iota\right)],\forall (A:\mathrm{Matrix}\left(iota,iota,\mathbb{R}\right)),\mathrm{lambdaMin}\left(A\right)=ifhA:\mathrm{Matrix}.\mathrm{IsHermitian}\left(A\right)then(ifh:\mathrm{Finset}.\mathrm{Nonempty}\left((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(iota\right))\right)then\mathrm{Finset}.{\inf }^{\prime }\left((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(iota\right)),h,hA.eigenvalues\right)else0)else0$$

Formalization. D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.lambdaMin (✓ std3).

Citation. Anuj Apte; Ojas Parekh; James Sud (2025). Conjectured Bounds for 2-Local Hamiltonians via Token Graphs. URL: https://arxiv.org/abs/2506.03441v2.

Commentary.

Page 9: “Let λ_max(·), λ_min(·), and eigs(·) describe the maximum eigenvalue, minimum eigenvalue, and the set of unique eigenvalues of a matrix.” The adjacency matrix is real and Hermitian. The nonempty branch uses Finset.inf’ on Matrix.IsHermitian.eigenvalues, the real eigenvalues with multiplicity. Its dependent proof arguments hA and h appear explicitly. The empty-carrier and non-Hermitian extensions are zero; neither extension is used in the counterexample.

Definition 1.5 (Conjecture 7).

$$(claim)\iff (\forall (n:\mathbb{N}),\forall (G:\mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right)),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)],\forall (k:\mathbb{N}),(1\le k)\Rightarrow ((k\le \mathrm{Nat}.\mathrm{div}\left(n,2\right))\Rightarrow (-\frac{(\mathrm{maxCut}\left(G\right):\mathbb{R})+(\mathrm{maxMatchingLe}\left(G,k\right):\mathbb{R})}{2}\le \mathrm{lambdaMin}\left(\mathrm{SimpleGraph}.\mathrm{adjMatrix}\left(\mathbb{R},\mathrm{tokenGraph}\left(G,k\right)\right)\right))))$$

Formalization. D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.claim (✓ std3).

Citation. Anuj Apte; Ojas Parekh; James Sud (2025). Conjectured Bounds for 2-Local Hamiltonians via Token Graphs. URL: https://arxiv.org/abs/2506.03441v2.

Commentary.

Appendix D.2, page 39: “In contrast, the following bound was shown to hold on our dataset”; “Conjecture 7. For all G and for all 1 ≤ k ≤ ⌊n/2⌋” followed by “λ_min(A(F_k(G))) ≥ −(C(G)+M_k(G))/2.” The formula quantifies all finite simple graphs with decidable adjacency, with unit edge weights. This is a specialization of the source’s all-graphs assertion. Fin n labels the n vertices; Nat.div n 2 is floor(n/2). The tokenGraph is the existing finite-subset graph: two equally sized subsets differ by one token moved along an edge. The natural cut and matching cardinalities are coerced to real numbers before division by two. No connectedness or bipartiteness hypothesis is imposed.

Lemma 1.6 (Real and complex adjacency matrices).

$$\forall (n:Type),[\mathrm{Fintype}\left(n\right)],[\mathrm{DecidableEq}\left(n\right)],\forall (G:\mathrm{SimpleGraph}\left(n\right)),[\mathrm{DecidableRel}\left(\mathrm{SimpleGraph}.\mathrm{Adj}\left(G\right)\right)],\mathrm{Matrix}.\mathrm{map}\left(\mathrm{SimpleGraph}.\mathrm{adjMatrix}\left(\mathbb{R},G\right),\mathrm{Complex}.\mathrm{ofReal}\right)=\mathrm{SimpleGraph}.\mathrm{adjMatrix}\left(\mathbb{C},G\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.adjMatrix_complex_map (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Anuj Apte; Ojas Parekh; James Sud (2025). Conjectured Bounds for 2-Local Hamiltonians via Token Graphs. URL: https://arxiv.org/abs/2506.03441v2.

Commentary.

Mapping the real zero-one adjacency matrix entrywise by Complex.ofReal gives the complex adjacency matrix. This identity lets lambdaMin40 apply the complex Rayleigh estimate to the real adjacency matrix.

Theorem 1.7 (A phase test contradicts the bound).

$$\neg claim$$

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

Resolves. Problems/apte-parekh-sud-2025-token-graph-cut-bound (refuted) by D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.result.

Source. Repository-derived.

Acknowledgement. Anuj Apte; Ojas Parekh; James Sud (2025). Conjectured Bounds for 2-Local Hamiltonians via Token Graphs. URL: https://arxiv.org/abs/2506.03441v2.

Commentary.

Take the five-cycle blow-up with five independent blocks of size 40 and complete bipartite edges between successive blocks. Its 100-token graph uses the existing tokenGraph. Put z = (−4+3i)/5 and multiply z to the block index over the occupied vertices. Each phase has modulus one. Each oriented edge of the original graph occurs as a token move in choose(198,99) token subsets, so the energy reduces to a sum over the original graph. The squared norm is choose(200,100), and the ratio of these binomial coefficients is 50/199. The real part of the edge-phase sum is 2·40²·(4 Re z + Re z⁴), with 4 Re z + Re z⁴ = −2527/625. The quotient is −646912/199. Splitting the complex phase vector into its real and imaginary parts connects this quotient to the least eigenvalue of the real adjacency matrix. The cut weight is affine in each block occupancy; rounding each occupancy to zero or 40 gives at most four cut cycle edges, hence maximum cut at most 6400. The matching weight is at most 100. The conjectured lower bound is therefore at least −3250, whereas the least eigenvalue is at most −646912/199, smaller by 162/199.

References

• Truth anchor: D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.adjMatrix_complex_map
• Truth anchor: D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.claim
• Truth anchor: D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.crosses
• Truth anchor: D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.lambdaMin
• Truth anchor: D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.maxCut
• Truth anchor: D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.maxMatchingLe
• Truth anchor: D5/S3/Combinatorics/Graph/TokenGraph/CutBoundRefutation.result
• Dependency: D5/S3/Combinatorics/Graph/TokenGraphLaplacianRadiusRefutation