Metadata
slug: coutinho-baptista-2023-normalized-laplacian-tree-state-transfer-refutation
bibkey: coutinhobaptista2023normalized
doi: 10.1080/03081087.2023.2236282
url: https://arxiv.org/abs/2209.04668v1
triage: theorem
motivation_gids:
- D5/S3/Quantum/Dynamics/NormalizedLaplacianTreeStateTransfer.result
A seventeen-vertex tree admits normalized-Laplacian perfect state transfer
Problem
G. Coutinho and P. F. Baptista, Quantum Walks in the Normalized Laplacian, arXiv:2209.04668v1 (2022; journal publication online 2023, DOI 10.1080/03081087.2023.2236282), Conclusion, norm-laplacian-v2.tex, line 427:
For trees, we were not able to show a complete analogous result to the combinatorial Laplacian case — that is, that perfect state transfer does not occur. We were however able to significantly restrict the possible cases, and therefore we conjecture that apart from the paths on and vertices, no tree admits perfect state transfer according to the normalized Laplacian.
This quotation was checked against the v1 TeX source, md5 b274bca76e7a9e881ea5b092556075a9. The definitions preceding equation (1), lines 89–98, and the transfer definition, lines 161–164, use , and for a complex unit . See also the literature note.
Issue #20154 fixes the statement: for every natural number , every simple graph on with decidable adjacency, and every pair of distinct vertices , if is a tree then there are no and with and . This is claim, and it is refuted. The two- and three-vertex trees are precisely the excluded paths.
Motivation
The source studies trees as quantum-network architectures requiring few edges. Excluding transfer on all larger trees would extend the combinatorial-Laplacian obstruction to the normalized-Laplacian walk. A tree supporting transfer distinguishes these Hamiltonian models and shows that acyclicity alone does not prevent exact transfer in the normalized model.
Gap
The bounded literature check recorded in #20154 reports:
- The orchestrator found only arXiv v1; the journal text was not read.
- Semantic Scholar listed two citing works. The orchestrator read their TeX and reported that Kong, Wyman and Xi (2024, arXiv:2401.06022) mention state transfer only in their introduction, while Wyman and Xi (2023, arXiv:2304.04659) do not discuss it. OpenAlex counted no citations of the journal version.
- The orchestrator’s arXiv abstract search for both “normalized Laplacian” and “state transfer” returned the source and Alvir et al. (2016, arXiv:1409.5840). No settlement was found in that search or in the repository’s Problems, Library and issue search.
- The search seat reported that a characteristic-polynomial formula of Das–Sun (2016, Taiwanese Journal of Mathematics 20, 491–507), combined with the source’s characterization, yields this transfer. That prior-implication reading was not independently reproduced here; no claim of a new spectral formula or exhaustive priority is made.
not-found-in-searched-scope refers to an explicit settlement of the conjecture within that recorded search scope.
Route
Let be adjacent to two leaves and to , and let each be adjacent to one further leaf . These are all the edges. The graph has vertices and edges, every vertex is reachable from , and its degrees are at , at each , and at the leaves. In the Lean graph, , , , and for .
- The antisymmetric mode. has normalized-Laplacian eigenvalue .
- The symmetric modes. Write a vector constant on the seven arms by its entries . Four eigenvectors are , , and , with eigenvalues given by their subscripts. The exact decomposition is .
- The phases. At , the four symmetric phases are , whereas the antisymmetric phase is . Thus fixes and negates .
- Transfer. Since is half the sum of these two vectors, . The private declarations
tree_isTreeandtransfersupply the tree and transfer certificates used byresult : ¬ claim.
Falsifier
The counterexample must use the source’s Hamiltonian and exact coordinate-state transfer. The module defines:
normalizedLaplacianby multiplying the combinatorial graph Laplacian on both sides by the diagonal inverse square roots of the degrees, as a complex matrix;walkwith the source’s positive sign, ;PSTby existence of a real time and a scalar of norm one giving equality of the entire evolved coordinate vector with the target coordinate vector;claimwith the universal quantifiers, tree hypothesis, lower bound and distinctness condition stated above.
The normalized-Laplacian definition extends to isolated vertices using inverse zero; a tree on at least four vertices has none. PST does not require a positive time, but the exhibited time is positive. The witness has phase and exact vector equality, so it also meets the source’s transfer definition without a numerical tolerance or an ambiguity about global phase.
Evidence
The canonical source is D5/S3/Quantum/Dynamics/NormalizedLaplacianTreeStateTransfer.lean (267 lines).
- Proof. It proves
result : ¬ claim. - Reuse. It applies
EnergyEigenstateStationarity.exp_mulVec_of_eigenvectorto the certified modes and combines their evolutions by matrix-vector linearity. - Axioms. It uses only the standard axioms
propext,Classical.choiceandQuot.sound; nosorry,native_decide, or new axiom. - Escape registrations.
resultis the designated refutation result of theutilityheader and is exempt. The module has no other public theorem.
Frozen state: Golden/Frozen/state/D5/S3/Quantum/Dynamics/NormalizedLaplacianTreeStateTransfer.lean.json, statement sha256:3b5928f1a3c40af655086887455794fc884a1ccf7b230212cb5ba99d64e07b3e.
Declaration statements:
result:sha256:87e58f30451611d0a6ae70ebbad14e191797af13f8cc38c93c86aef658c9a6bd;claim:sha256:4e576d6b7aea4437b44da5583e95bfe42c50615af040b9daaa8f0292b7c0e906.
Triage
Tier 1 conjecture of a 2022 preprint (journal publication online 2023), preregistered in issue #20154 before any Lean.
theorem; resolution refuted.
The module is admitted under the open-problem-resolution basis of CLAUDE.md §3.2; no escape witness is claimed, and the per-declaration proof shapes are listed in the delivery PR. The refutation is a certified instance with basis refutes. There is no digestion atom.
What the settlement shows
Proved by result: the universal assertion that every finite simple tree on at least four vertices forbids perfect state transfer between distinct vertices is false, with precisely the graph, real-time and unit-phase conventions of claim above. This is ¬ claim.
Computed, not formalized (independent Python/SymPy and NumPy/SciPy calculations):
- Exact arithmetic gives the full -vertex spectrum . The four symmetric eigenvectors, endpoint decomposition and exact spectral evolution give and . The full-spectrum assertion is not a theorem of the module.
- For the analogous tree with length-two arms and the same two leaves, numerical diagonalization at and gives maximum coordinate errors from of and , respectively. These are floating-point checks.
- For the tested values , perfect transfer was not observed on the grid . The largest sampled transfer amplitudes were respectively , and . This grid excludes no untested time or tree.
- A symbolic determinant for the arm-symmetric normalized-adjacency block, with , is .
Argued, not formalized.
- Failure mechanism. The irrational eigenvalues in the full spectrum do not obstruct these endpoints. Arm-difference vectors have zero entries at ; if their arm coordinates satisfy , the normalized adjacency acts by . This invariant subspace has normalized-Laplacian eigenvalues and is orthogonal to both endpoint states. Only the rational symmetric modes and the antisymmetric eigenvalue enter the transfer. Acyclicity does not exclude their exact phase alignment.
- A family and its phase obstruction. For an integer , the analogous tree has vertices and central degree . On the orthonormal basis , normalized adjacency has zero diagonal and consecutive off-diagonal entries . Expanding its tridiagonal determinant gives , so the symmetric normalized-Laplacian eigenvalues are . All off-diagonal entries are nonzero: an eigenvector with zero first coordinate would have all coordinates zero by successive row equations. Consequently all four eigenvalues occur in the symmetric endpoint support. Together with , this accounts for the endpoint states. Transfer requires the common symmetric phase to be because eigenvalue occurs, and the antisymmetric phase to be . Hence for an odd integer , and must both be even integers. Equivalently is an odd integer. Therefore is rational, hence an integer because is an integer, and it is odd. Conversely, if for an odd integer , then gives all four symmetric phases and the antisymmetric phase . Thus, for this family and this leaf pair, transfer occurs exactly when is an odd square; gives vertices. This family argument is not part of
result. It identifies as the smallest member of this family admitting that transfer, without deciding the smallest counterexample among all trees. - Surviving restrictions and open cases. The source’s tree corollary, TeX lines 391–394, states: “Let be a tree on three or more vertices, admitting perfect state transfer between vertices and . If and are in the same bipartite class, then they are leafs attached to the same vertex.” The witness has exactly those two leaves and satisfies this necessary restriction. A non-transfer condition excluding an odd-square central degree works for this leaf pair within the family by the preceding argument; extending such a condition to arbitrary trees is open. A classification of all transferring trees, existence of a smaller counterexample outside this family, and transfer between opposite bipartite classes in trees larger than are not settled here.
- Effect on the paper. The conjecture is in the final Conclusion paragraph; no preceding theorem uses it as a premise. The counterexample overturns that conjecture and meets the paper’s same-class restriction. The source also states at TeX line 425, citing Alvir et al. (2016, arXiv:1409.5840): “perfect state transfer occurs if and only if the path has or vertices.” This path statement is unaffected: the witness has a degree- vertex and is not a path. The source’s preceding spectral characterization and necessary tree restrictions are not replaced by a classification of all trees through this settlement.
ASSUMED-UNVERIFIED
The bounded literature check in #20154 does not establish exhaustive worldwide novelty or priority. The journal version, the full texts of the two citing works, the original arXiv search, the Semantic Scholar and OpenAlex counts, and the repository-wide search reported there were not independently reproduced here. The citing works’ author metadata were checked on arXiv; their reported contents remain attributed to the preregistration’s orchestrator. The Das–Sun prior-formula reading and its implication reported by the search seat were not reproduced. The independent checks above reproduce the registered witness and selected family computations, not the original computation scripts or grid specification in #20154.
The source’s SAGE/CoCalc search concerning trees through vertices (TeX line 415) was not reproduced. The path theorem quoted from the source was not independently checked in Alvir et al.; it and the source’s other general spectral and tree results are literature statements, not conclusions formalized by this module. All full-spectrum, numerical, symbolic-family and explanatory assertions labelled “Computed, not formalized” or “Argued, not formalized” remain outside the Lean settlement. The family-wide characterization, global minimality and the remaining tree-classification questions are not formal claims of result.