Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


slug: coutinho-guo-schmeits-2025-laplacian-peak-transfer-trees bibkey: coutinho2025peak doi: 10.48550/arXiv.2505.11986 url: https://arxiv.org/abs/2505.11986v4 triage: theorem motivation_gids:

  • D5/S3/Quantum/Dynamics/LaplacianPeakTransferTrees.result

Infinitely many non-star trees admit Laplacian peak state transfer

Problem

Gabriel Coutinho, Krystal Guo and Vincent Schmeits, Peak state transfer in continuous quantum walks, arXiv:2505.11986v4, Section 7, Open Problem 7.1 (p. 21), ask:

Determine whether infinitely many such trees, not isomorphic to the star graph, admit Laplacian peak state transfer.

Figure 10 (p. 22) includes a root with three hubs and two leaves per hub. For the real Laplacian , Section 3 defines and , summing over distinct eigenvalues and taking absolute values entrywise. Peak transfer between distinct vertices means at some real time. The source does not require that value to equal one.

Motivation

Proved: D5/S3/Quantum/Dynamics/LaplacianPeakTransferTrees.result proves claim: arbitrarily large finite trees, excluded from every star isomorphism class , have distinct vertices with Laplacian peak transfer. Preregistration #14801 names this settlement LPST-1. The settling Scribe node records OpenProblemResolutionClaim with resolution Proved.

Gap

The source supplies stars and one small non-star example, rather than an unbounded family. Arbitrarily large orders in the Lean conclusion imply infinitely many isomorphism classes. The claim includes all natural lower bounds, connectedness and acyclicity, exclusion of every , and the source’s spectral bound and exponential conventions.

Route

For a positive odd natural number , put , , and . Join a root to hubs, and each hub to leaves. The degrees are ; connectedness and edges prove that this is a tree. Both the root and a hub have degree at least two, excluding a star. Relabelling gives a graph on Fin n.

On vectors constant on the root, hubs and leaves, the Laplacian acts by

Its relevant eigenvalues are , and . The explicit eigenvectors have cell values , and , and

The root-to-hub projection entries are , and . For odd , the three phases at are , so all contributions to have the same phase. This realizes the alignment criterion described in the source’s Lemma 5.2.

The private declarations root_decomposition and phases and their consumers lead to tree_peak; result takes for every lower bound . The frozen EnergyEigenstateStationarity.exp_mulVec_of_eigenvector is used by real_eigenvector_exp for the matrix exponential action. lapPropagator uses ProjectionProbabilityFlow.hamiltonianPropagator at ; RationalWeightPathTransfer.hamiltonianPropagator_neg supplies the private conversion to the source expression in root_evolution.

Falsifier

The settlement would fail its stated criterion if the public spectral or exponential definitions differed from Section 3, an odd positive parameter failed to attain the bound, or the preregistration’s literature scope already contained a settlement. The Lean definitions follow the binding conventions of #14801; result : claim carries no additional hypotheses. Numerical samples support the construction but do not replace its proof.

Evidence

The kernel evidence is the settling module and its Scribe. Every theorem and lemma, including result, has proof shape bind-only after inlining: the root decomposition uses rational normalization, the phases use parity and exponential identities, and their consumers apply frozen or Mathlib facts and normalize. No escape witness survives the bypass test. Admission is open-problem-resolution (#14801; Proved). Utility is none: the result and helpers concern symbolic parameters and unbounded orders, with no fixed numerical certificate, finite enumeration, executable checker or numeric-reduction declaration.

The escape registration of result is DTR-Declared with declared_validated at Reg/D5/S3/Quantum/Dynamics/LaplacianPeakTransferTrees.lean. The compiled registration selects the graph operand of IsTree through the enrolled DependentFamily template, with a source-equivalence bridge and open continuation. .unknown marks an unknown residual and proves no undecidability or inexhaustibility.

Experiment entry: trureturing-experiments@602ec65402d492351ebc19230b04caa93001cda8, numerical check. The entry’s check.py has SHA-256 64d43c273db0a1935d94840271e9795b5937df9fb5283f8e687546b813c90542. Command: OPENBLAS_NUM_THREADS=1 VECLIB_MAXIMUM_THREADS=1 python3 /Users/auric/trureturing-experiments/docs/reports/coutinho-guo-schmeits-2025-laplacian-peak-transfer-trees/check.py. Exit code: 0. The full Laplacian is tested for at ; the even cases additionally use 2001 equally spaced times in . Eigenvalue grouping tolerance is .

distinct eigenvalues
11060.5333333333330.533333333333
25060.3600000000000.320000000000
317060.2689075630250.268907563025
444260.2136752136750.209150326797
596260.1769041769040.176904176904

The odd-case absolute discrepancies are respectively , and . The grid maxima for are respectively and . These are floating-point readings over the stated finite scope.

Triage

What the settlement shows

  • Proved, kernel: lap_cell gives the invariant cell-constant subspace. w0_eigen, wa_eigen and wb_eigen give eigenvalues . root_decomposition places in their span.
  • Proved, kernel and algebraic argument: hub_projection gives the coefficients , , . For , and both numerators are positive; the signs are therefore . The kernel helper bounds the latter magnitudes nonnegatively; strict positivity follows from and .
  • Proved, kernel: phases gives for odd at ; tree_peak proves attainment of the triangle bound at that time.
  • Proved, kernel and algebraic argument: tree_bound gives . Since , simplifying yields . Moreover as . The Section 3 triangle bound thus bounds the root-to-hub transfer probability by : this family has no uniform positive root-to-hub transfer probability. This does not rule out other vertex pairs or other families. The defining root-hub edge makes the transfer distance exactly one; these limit and distance conclusions are mathematical arguments here, not additional public Lean theorems.
  • Computed: for , the experiment entry in Evidence gives gaps at of and approximately , and grid maxima and . The computed non-attainment applies only to and the stated grid, not to every real time or every even parameter.
  • Open: an infinite non-star tree family with Laplacian peak transfer at distance at least two; no such conclusion is in result.
  • Open: an infinite non-star tree family with peak-transfer probability bounded below by a common positive constant.
  • Open: classification of Laplacian peak state transfer in trees.
  • Open: the source’s adjacency-dynamics question on trees.

Proved: the order strictly increases, by order_strictMono. The first member is the source’s 10-vertex example; treeFin_isTree and treeFin_not_star certify all positive parameters as non-star trees. Odd positive parameters give the unbounded peak-transfer family, settling the named infinitude question. The source’s bounding matrix and phase criterion keep their stated scope; the other questions listed above receive no settlement from this result. Uniform attainment or non-attainment for even parameters is open beyond the finite computed scope.

ASSUMED-UNVERIFIED

Literature currency beyond the arXiv and MathDB scope recorded in #14801 is unverified by this implementation seat. The preregistration supplies the source and literature attestation; no broader novelty claim is made. The four-slot escape registration is DTR-Declared with declared_validated, a source-equivalence bridge and open continuation; .unknown marks an unknown residual and proves no undecidability or inexhaustibility.