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
- Absolute and Conditional Convergence; Rearrangement; Products
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Analyticity of Holomorphic Functions; Liouville and Morera
- Approximation and Compactness in C(K)
- Arc Length and Rectifiable Curves
- Banach Alaoglu Goldstine and Krein Milman
- Banach Algebras Spectrum and Holomorphic Functional Calculus
- Banach Valued Integration and the Radon Nikodym Property
- Banach-Space Differential Calculus and Banach Manifolds
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Bounded Variation and the Riemann–Stieltjes Integral
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Coordinate and Path Transport
- Complex Differentiability and the Cauchy–Riemann Equations
- Complex Norms and Realification
- Complex Subspace Realification
- Complexification, Realification and Real Structures
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Continuous Functional Calculus for Self Adjoint and Normal Operators
- Contour Integration
- Convergence: Nets and Filters
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Cyclic Groups and Direct Products
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces Adjoint Operators and Annihilators
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Foundations of the Real Numbers for Analysis
- Function Space Topologies and the Exponential Law
- Fundamental Trigonometric Identities
- Gelfand Theory and Commutative C Star Algebras
- Goursat's Theorem and Cauchy's Theorem in a Convex Domain
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group C Star Algebras and the Fell Unitary Dual
- Group Homomorphisms and the Isomorphism Theorems
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lieb–Robinson locality, clustering and gapped spectral transport
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Line Integrals and the Gradient Theorem
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Local spin matrix algebras and isometric inclusions
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal density states and spectral moments
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Partitions of Unity and Paracompactness
- pi: the Equivalent Characterizations
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Properties of the Integral and the Working FTC
- Pure and Mixed States, Ensembles, and Schmidt Decomposition
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Splitting Fields
- Stone–Weierstrass in General
- Strongly Continuous Semigroups and Hille Yosida
- Subspaces, Products, and Quotients
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Analytic Hahn Banach Theorem
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Fundamental Theorem of Algebra
- The Fundamental Theorem of Finite Abelian Groups
- The Fundamental Theorems of Calculus
- The Galois Correspondence
- The Lebesgue Integral and the Convergence Theorems
- The Riemann Integral: Definition and Integrability
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Uniformly bounded finite-range quantum spin interaction
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
None yet.
5 · Examples, experiments and counterexamples
A one-spin path can close its spectral gap
Statement
Let one site of have spin dimension , let , and define the finite-volume Hamiltonian path on , with all other interaction terms zero. This is a finite-range path with a uniform finite weighted-interaction norm and gapped endpoint Hamiltonians, but its gap closes at . Thus endpoint gaps alone do not imply a uniform path gap.
Statement references
Facts & Assumptions
Given: A single spin space , the path in the Statement, and the weighted-interaction convention. Energies are dimensionless in the chosen positive energy unit, , and is dimensionless.
Weighted interactions and gapped finite-volume paths: a one-site self-adjoint matrix path with a bounded coefficient is a finite-range path with finite -interaction and derivative norms.
Proof
Given: and .
The interaction has only one nonzero term, on a singleton support, with coefficient ; its derivative is the constant . The two weighted norms are finite because the support and coefficient are bounded and every admissible weight is positive at distance zero.
The eigenvalues of are and . The ground eigenvalue is , the excited eigenvalue is , so the gap is . It is at each endpoint and at . The path therefore has gapped endpoints but no uniform positive gap on .
A degenerate gapped Ising ground mixture does not cluster
Statement refuted
Assume Countable Choice and the finite-matrix -identity. For each finite , let with the canonical unital tensor-factor inclusions, and let in operator norm. A uniformly bounded finite-range interaction assigns self-adjoint terms to finite nonempty supports ; for some finite , , and , if or , where , and . Its free-boundary finite-volume Hamiltonian and dynamics are and ; is the strongly continuous norm-limit group on local observables. A state is a bounded complex-linear functional with and for every . A positive-energy ground-state representation consists of a contractive unital -representation on a complex Hilbert space, a unit vector , and a strongly continuous unitary group such that , , and for every . Its strong generator is : the norm derivative exists exactly for in a dense domain and equals there, where and for every . The spectrum is the set of for which has no bounded everywhere-defined inverse. An excitation gap in this representation means .
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- chain on , even when . In particular, for each such state there must be constants and such that
where is the Pauli observable on site .
Statement references
Facts & Assumptions
Given: Countable Choice, the quasi-local spin- algebra on with its finite-matrix -identity, and dimensionless energy and time units with .
Countable Choice supplies the norm completions; the finite-matrix -identity is supplied, not an unrestricted choice assumption. The Axiom of Countable Choice () Finite matrix C-star algebra and density-state duality
Local spin factors are finite matrix algebras, their inclusions are isometric and their norm completion is the quasi-local -algebra. Local spin matrix algebras and their factor inclusions Norm-completed quasi-local quantum spin algebra Quasi-local algebra completion and locality
Bounded finite-range interactions have the stated thermodynamic norm-limit dynamics. Uniformly bounded finite-range quantum spin interaction Strongly continuous thermodynamic spin automorphism group
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
Dominated convergence applies to summable nonnegative majorants on a countable set and to scalar finite-measure integrals. Dominated convergence
The complex exponential has derivative itself. The continuous-curve fundamental theorem on a real interval therefore gives for , and hence . 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 and zero terms on other supports.
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 . It satisfies the finite-range hypotheses in [F2], so its thermodynamic dynamics exists. This conclusion requires no choice of a finite-volume ground state.
Let be the set of finite subsets of . It is countable under [A1], by enumerating finite tuples and taking their ranges. Complete the finitely supported complex functions on for their linear-first sum inner product, obtaining by [F3]. Denote its orthonormal basis by . Define Here , 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 . On a finite region , decompose into the subspaces with fixed and fixed finite ; each has the basis vectors indexed by and is a standard matrix representation of . Therefore locally. These compatible representations extend by norm continuity and [F3] to a unital contractive -representation of .
For , put . This number is finite, is zero exactly when , 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 . Define the diagonal operator Finite-support vectors make the domain dense and the quadratic form is nonnegative. If lies in the adjoint domain with , testing on each basis vector gives , so . Conversely that square-summability condition makes the adjoint identity hold by sum Cauchy–Schwarz. Thus on exactly this domain.
Set . It is a unitary group. For each , dominated convergence with majorant proves strong continuity. For , and [F4] show its norm derivative at zero is . Conversely, if that norm derivative exists, its coordinates must be , whose square sum is finite, so the exact generator domain is . The kernel has basis . Every other diagonal energy is at least two and energy two occurs for a singleton . For , the diagonal inverse is bounded by and maps into since is bounded. The same diagonal argument excludes negative real and nonreal spectrum. Consequently , with excitation gap exactly two.
The representation is covariant for the actual dynamics in step 1.1. Every interaction term is diagonal in the Pauli 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 is constant. On the phase of is ; the energy difference involves only the two bonds adjacent to . 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 , and the norm completion gives This verifies the relation to the thermodynamic dynamics rather than choosing an unrelated diagonal operator.
Let . It is a unit zero-energy vector fixed by , so its state is a positive-energy ground state. Its finite restrictions have density with the empty-region density one; these are the consistent equal mixture of the two product phases. This representation is cyclic. Given finite and , choose and let . Then 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.
In the two product vectors has respective expectations and , whereas has expectation one in each for . Hence the equal mixture has and . For every integer its connected correlation is therefore one. No finite and positive can satisfy for all . 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
- S. Bachmann, S. Michalakis, B. Nachtergaele, and R. Sims, Automorphic Equivalence within Gapped Phases of Quantum Lattice Systems, §2 and discussion after Theorem 5.5
- Bruno Nachtergaele and Robert Sims, Lieb–Robinson Bounds and the Exponential Clustering Theorem, arXiv:math-ph/0506030v3; section 4, PDF pp. 10–11, degenerate-ground-space qualification as context only; the Ising example and its cyclic representation are constructed locally. Full 12-page article retrieved and read.