Alphabeta Math
Pipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Lieb–Robinson locality, clustering and gapped spectral transport — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

A one-spin path can close its spectral gap

Statement

Let one site of Zd have spin dimension 2, let Z=diag(1,−1), and define the finite-volume Hamiltonian path H(s)=(1−2s)Z on 0≤s≤1, with all other interaction terms zero. This is a C1 finite-range path with a uniform finite weighted-interaction norm and gapped endpoint Hamiltonians, but its gap closes at s=12. Thus endpoint gaps alone do not imply a uniform path gap.

Facts & Assumptions

Given: A single spin space C2, the path in the Statement, and the weighted-interaction convention. Energies are dimensionless in the chosen positive energy unit, ℏ=1, and s is dimensionless.

[F1]

Weighted interactions and gapped finite-volume paths: a one-site self-adjoint matrix path with a bounded C1 coefficient is a finite-range path with finite G-interaction and derivative norms.

Proof

technique · direct

Given: H(s)=(1−2s)Z and Z=(100−1).

1.1givenF1algebra

The interaction has only one nonzero term, on a singleton support, with coefficient 1−2s; its derivative is the constant −2. The two weighted norms are finite because the support and coefficient are bounded and every admissible weight is positive at distance zero.

2.1givenstep 1.1algebra∎

The eigenvalues of H(s) are 1−2s and −(1−2s). The ground eigenvalue is −∣1−2s∣, the excited eigenvalue is +∣1−2s∣, so the gap is 2∣1−2s∣. It is 2 at each endpoint and 0 at s=12. The path therefore has gapped endpoints but no uniform positive gap on [0,1].

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passverified 2026-10-22 (gpt-6.1-sol)Open item page →

A degenerate gapped Ising ground mixture does not cluster

Statement refuted

Assume Countable Choice and the finite-matrix C∗-identity. For each finite Λ⊂Z, let AΛ=⨂j∈ΛM2(C) with the canonical unital tensor-factor inclusions, and let A=⋃∣Λ∣<∞AΛ‾ in operator norm. A uniformly bounded finite-range interaction Φ assigns self-adjoint terms Φ(Z)∈AZ to finite nonempty supports Z; for some finite M≥1, R≥0, and κ<∞, Φ(Z)=0 if ∣Z∣>M or diam⁡∞Z>R, where diam⁡∞Z:=max⁡x,y∈Z∣x−y∣, and sup⁡x∑Z∋x∥Φ(Z)∥≤κ. Its free-boundary finite-volume Hamiltonian and dynamics are HΛ=∑∅≠Z⊆ΛΦ(Z) and αtΛ(A)=eitHΛ/ℏAe−itHΛ/ℏ; αt is the strongly continuous norm-limit group on local observables. A state is a bounded complex-linear functional ω:A→C with ω(1)=1 and ω(A∗A)≥0 for every A∈A. A positive-energy ground-state representation consists of a contractive unital ∗-representation π:A→B(H) on a complex Hilbert space, a unit vector Ω∈H, and a strongly continuous unitary group (Ut)t∈R such that ω(A)=⟨π(A)Ω,Ω⟩, UtΩ=Ω, and π(αt(A))=Utπ(A)Ut∗ for every A∈A. Its strong generator is iK: the norm derivative lim⁡t→0(Utx−x)/t exists exactly for x in a dense domain D(K) and equals iKx there, where K=K∗ and ⟨Kx,x⟩≥0 for every x∈D(K). The spectrum σ(K) is the set of z∈C for which K−z:D(K)→H has no bounded everywhere-defined inverse. An excitation gap g>0 in this representation means σ(K)⊆{0}∪[g,∞).

The claim refuted here is that a nonzero excitation gap alone forces ordinary exponential connected clustering for every positive-energy ground state of a uniformly bounded finite-range spin-12 chain on Z, even when dim⁡ker⁡K>1. In particular, for each such state ω there must be constants C0<∞ and μ>0 such that

∣ω(Z0Zr)−ω(Z0)ω(Zr)∣≤C0e−μr(r=1,2,…),

where Zj=diag⁡(1,−1) is the Pauli observable on site j.

Facts & Assumptions

Given: Countable Choice, the quasi-local spin-12 algebra on Z with its finite-matrix C∗-identity, and dimensionless energy and time units with ℏ=1.

[A1]

Countable Choice supplies the norm completions; the finite-matrix C∗-identity is supplied, not an unrestricted choice assumption. The Axiom of Countable Choice (ACω) Finite matrix C-star algebra and density-state duality

[F1]

Local spin factors are finite matrix algebras, their inclusions are isometric and their norm completion is the quasi-local C∗-algebra. Local spin matrix algebras and their factor inclusions Norm-completed quasi-local quantum spin algebra Quasi-local algebra completion and locality

[F2]

Bounded finite-range interactions have the stated thermodynamic norm-limit dynamics. Uniformly bounded finite-range quantum spin interaction Strongly continuous thermodynamic spin automorphism group

[F3]

The completion of an inner-product space is Hilbert under Countable Choice; bounded operator spaces are complete. The norm completion of an inner-product space is a Hilbert space If (Y) is Banach then (\mathcal B(X,Y)) is Banach

[F4]

Dominated convergence applies to summable nonnegative majorants on a countable set and to scalar finite-measure integrals. Dominated convergence

[F5]

The complex exponential has derivative itself. The continuous-curve fundamental theorem on a real interval therefore gives eitw−1=∫0tiweiswds for w≥0, and hence ∣eitw−1∣≤∣t∣w. The complex exponential is entire and its complex derivative is itself Fundamental theorem of calculus for Banach-valued continuous curves

Counterexample

Given: [A1], [F1]–[F5]; use the interaction Φ({j,j+1})=(I−ZjZj+1)/2 and zero terms on other supports.

1.1A1F1F2givenconstructalgebra

Each interaction term is an orthogonal projection of norm one. The interaction is self-adjoint, has support size two, range one and per-site sum κ=2. It satisfies the finite-range hypotheses in [F2], so its thermodynamic dynamics αt exists. This conclusion requires no choice of a finite-volume ground state.

1.2A1F1F3givenconstructalgebra

Let F be the set of finite subsets of Z. It is countable under [A1], by enumerating finite tuples and taking their ranges. Complete the finitely supported complex functions on {+1,−1}×F for their linear-first sum inner product, obtaining H=ℓ2({+1,−1}×F) by [F3]. Denote its orthonormal basis by ∣σ,F⟩. Define π(Zj)∣σ,F⟩=σ(−1)1F(j)∣σ,F⟩,π(Xj)∣σ,F⟩=∣σ,F△{j}⟩. Here X=(0110), and △ denotes symmetric difference. These operators are self-adjoint unitaries, anticommute at the same site and commute at distinct sites. Thus they give the usual local Pauli matrix representations, including Yj=iXjZj. On a finite region Λ, decompose H into the subspaces with fixed σ and fixed finite F∖Λ; each has the 2∣Λ∣ basis vectors indexed by F∩Λ and is a standard matrix representation of AΛ. Therefore ∥π(A)∥=∥A∥ locally. These compatible representations extend by norm continuity and [F3] to a unital contractive ∗-representation of A.

2.1step 1.2constructalgebra

For F∈F, put w(F)=∣{j∈Z:1F(j)≠1F(j+1)}∣. This number is finite, is zero exactly when F=∅, and is at least two otherwise: a nonempty finite set has both a left and a right boundary. More precisely it is twice the number of finite interval components of F. Define the diagonal operator K∣σ,F⟩=w(F)∣σ,F⟩,D(K)={ξ:∑σ,Fw(F)2∣ξσ,F∣2<∞}. Finite-support vectors make the domain dense and the quadratic form is nonnegative. If ξ lies in the adjoint domain with K∗ξ=ζ, testing on each basis vector gives ζσ,F=w(F)ξσ,F, so ξ∈D(K). Conversely that square-summability condition makes the adjoint identity hold by sum Cauchy–Schwarz. Thus K=K∗ on exactly this domain.

3.1F4F5step 2.1constructalgebra

Set Ut∣σ,F⟩=eitw(F)∣σ,F⟩. It is a unitary group. For each ξ, dominated convergence with majorant 4∣ξσ,F∣2 proves strong continuity. For ξ∈D(K), ∣eitw−1∣/∣t∣≤w and [F4] show its norm derivative at zero is iKξ. Conversely, if that norm derivative exists, its coordinates must be iw(F)ξσ,F, whose square sum is finite, so the exact generator domain is D(K). The kernel has basis ∣+,∅⟩,∣−,∅⟩. Every other diagonal energy is at least two and energy two occurs for a singleton F. For 0<λ<2, the diagonal inverse (w(F)−λ)−1 is bounded by max⁡(1/λ,1/(2−λ)) and maps into D(K) since w/(w−λ) is bounded. The same diagonal argument excludes negative real and nonreal spectrum. Consequently σ(K)⊆{0}∪[2,∞), with excitation gap exactly two.

4.1F1F2step 1.1step 1.2step 2.1step 3.1algebra

The representation is covariant for the actual dynamics in step 1.1. Every interaction term is diagonal in the Pauli Z basis, and these terms commute. Finite-volume conjugation of a local observable therefore depends only on the finitely many bonds meeting its support. In particular the evolution of Zj is constant. On Xj∣σ,F⟩ the phase of Utπ(Xj)Ut∗ is eit(w(F△{j})−w(F)); the energy difference involves only the two bonds adjacent to j. It is exactly the phase from every finite-volume Hamiltonian containing these bonds. The local Pauli matrices generate every finite matrix algebra, so the covariance identity holds for every local A, and the norm completion gives π(αt(A))=Utπ(A)Ut∗(A∈A). This verifies the relation to the thermodynamic dynamics rather than choosing an unrelated diagonal operator.

5.1F1step 1.2step 3.1step 4.1constructalgebra

Let Ω=(∣+,∅⟩+∣−,∅⟩)/2. It is a unit zero-energy vector fixed by Ut, so its state ω(A)=⟨π(A)Ω,Ω⟩ is a positive-energy ground state. Its finite restrictions have density ρΛ=12∣+⋯+⟩⟨+⋯+∣+12∣−⋯−⟩⟨−⋯−∣, with the empty-region density one; these are the consistent equal mixture of the two product phases. This representation is cyclic. Given finite F and σ∈{+1,−1}, choose j∉F and let Pσ,j=(I+σZj)/2. Then 2 π(∏i∈FXi Pσ,j)Ω=∣σ,F⟩. Thus every displayed basis vector is generated by a local observable, proving cyclicity and identifying the gap in step 3.1 as a gap of the state's own ground representation.

6.1step 3.1step 5.1algebradischarge-contradiction∎

In the two product vectors Zi has respective expectations +1 and −1, whereas ZiZj has expectation one in each for i≠j. Hence the equal mixture has ω(Zj)=0 and ω(ZiZj)=1. For every integer r≥1 its connected Z0,Zr correlation is therefore one. No finite C0 and positive μ can satisfy 1≤C0e−μr for all r. The two product vector states are distinct positive-energy ground states, so uniqueness fails exactly where needed. This gives a gapped degenerate counterexample without altering any assertion about transport of an entire gapped ground band.

Remarks

The state is the equal mixture of the two ordered product phases on the quasi-local algebra. The proof does not assert a coherent infinite-volume GHZ wavefunction in a selected infinite tensor product. It constructs and checks the actual cyclic Hilbert representation, its generator and its two-dimensional zero eigenspace. The source's general degenerate-ground-space discussion supplies context only; the example is calculated locally.

Sources