Thermodynamic Spectral Gaps in Parameterized Quantum Lattice Systems

Contributions

Our contributions are the following.

1. We give separate definitions for literal finite-volume gaps, ground-band gaps, uniform finite-volume gaps, GNS bulk gaps, and uniform parameterized GNS gaps.

2. We prove an elementary compactness theorem for a constant-rank isolated spectral cluster and show why rank change invalidates the common compactness shortcut.

3. We give three explicit counterexamples: a norm-continuous compact matrix family with pointwise but nonuniform literal gaps, a locally continuous profinite spin family with uniform locality but collapsing GNS gaps, and a sequence of finite ferromagnetic chains whose gaps close in the thermodynamic limit.

4. We formulate a fibration of quantitative gap witnesses and its propositional image inside the Hamiltonian functor. The witness records enough data to make the predicate meaningful and stable under restriction of the parameter object.

5. We separate two established analytic mechanisms. Spectral flow transports a low-energy sector along a path already known to have a uniform isolated band. Perturbative gap stability preserves a pre-existing gap only under substantive structural hypotheses such as frustration freeness, quantitative local gaps, and LTQO.

6. We state formalization contracts for Lean and executable finite-model checks for Haskell. These artifacts represent hypotheses and finite calculations. They do not claim proofs of infinite-volume theorems.

Status vocabulary

We use five labels throughout:

The distinction is important. Formal vocabulary should expose uncertainty, not conceal it.

Local and quasi-local observables

Let $(\Gamma,d)$ be a countable metric space. We assume uniform local finiteness when a volume-growth estimate is required. Each site $x\in\Gamma$ carries a finite-dimensional Hilbert space $\mathcal H_x$. For a finite set $\Lambda\Subset\Gamma$, define

$$\mathcal A_\Lambda = \bigotimes_{x\in\Lambda}\mathcal B(\mathcal H_x).$$

If $\Lambda\subset\Lambda'$, the canonical inclusion is

$$\iota_{\Lambda,\Lambda'}(A)=A\otimes 1_{\Lambda'\setminus\Lambda}.$$

These maps are unital and isometric. The local algebra and its C*-completion are

$$\mathcal A_{\mathrm{loc}} = \bigcup_{\Lambda\Subset\Gamma}\mathcal A_\Lambda, \qquad \mathcal A_\Gamma = \overline{\mathcal A_{\mathrm{loc}}}^{\|\cdot\|}.$$

The formal infinite sum of all interaction terms is generally not an element of $\mathcal A_\Gamma$. Under decay hypotheses, the thermodynamic object is instead a strongly continuous automorphism group, often defined first on local observables and then extended.

F-functions and uniform locality

For an interaction $\Phi$, set

$$\|\Phi\|_F = \sup_{x,y\in\Gamma} \frac{1}{F(d(x,y))} \sum_{X\ni x,y}\|\Phi(X)\|.$$

Standard choices on $\mathbb Z^\nu$ are a sufficiently fast polynomial tail and its exponentially weighted version,

$$F(r)=\frac{1}{(1+r)^{\nu+\epsilon}}, \qquad F_a(r)=e^{-ar}F(r).$$

Local F-continuity is a finite-region condition. It does not include the separate geometric hypothesis $T_F(R)\to0$, which will be stated whenever a family-uniform thermodynamic limit is used.

Uniform locality and parameter continuity are distinct. Global norm continuity $S\to\mathcal B_F$ on compact $S$ implies uniform boundedness. It is often too strong for product-topology disorder because a change far from a fixed observation region can remain large in a supremum over all sites.

Uniform Lieb-Robinson control

The standard Lieb-Robinson argument yields a bound whose constants depend on the F-function, the geometry, and $\|\Phi\|_F$. A uniform family bound therefore gives constants independent of $s$.

Literal finite-volume ground-state gap

Let $H_\Lambda$ be self-adjoint on the finite-dimensional Hilbert space for $\Lambda$. Write

$$E_0(\Lambda)=\min\operatorname{spec}(H_\Lambda).$$

This definition is sensitive to a low-energy level that approaches the ground energy and becomes exactly degenerate in a limit.

Finite-volume ground-band gap

This is the natural finite-volume predicate for spectral flow. An isolated low-energy band can survive small internal splittings even when the literal ground-state gap becomes small.

Uniform finite-volume gap

The exhaustion and boundary convention cannot be suppressed. Open and periodic volumes can display different low-energy behavior.

GNS bulk gap

Let $\omega$ be an infinite-volume ground state for the dynamics $\tau$. Let $(\mathcal H_\omega,\pi_\omega,\Omega_\omega)$ be its GNS triple. The dynamics is implemented by a positive generator $H_\omega$ with $H_\omega\Omega_\omega=0$ [BratteliRobinson2].

If the GNS ground vector is unique, the positive gap can be expressed through a Poincare-type estimate on the domain of the generator. The representation and state remain essential data.

Uniform parameterized GNS gap

Pointwise positivity of $\gamma_{\mathrm{GNS}}(\omega_s)$ is not enough. Uniformity is a separate quantifier and is the physically relevant one for a single parameterized phase object.

A moving weak defect

Let $\Gamma=\mathbb N$ with one qubit at each site. Let $p_x=|1\rangle\langle1|_x$. Consider the product interactions whose formal Hamiltonians are

$$H_\infty=\sum_{x\geq1}p_x, \qquad H_n=\frac{1}{n}p_n+\sum_{x\neq n}p_x.$$

The parameter space $S=\mathbb N\cup\{\infty\}$ is profinite. On every fixed finite region, $H_n$ agrees with $H_\infty$ for all sufficiently large $n$. The family is locally continuous and uniformly finite range. Its Lieb-Robinson constants can therefore be chosen uniformly.

The family is not continuous in the global interaction norm that takes a supremum over all sites. This example explains why local parameter continuity and uniform locality should be stated separately.

Finite chains with a closing gap

For a length-$L$ open spin-$1/2$ ferromagnetic chain, let

$$H_L = \sum_{x=1}^{L-1}\frac{1-P_{x,x+1}}{2},$$

where $P_{x,x+1}$ swaps neighboring spins. Each summand is positive and the model is frustration free.

The infinite isotropic ferromagnetic chain is gapless. A theorem about all finite volumes must contain a lower bound independent of $L$ if it is to imply a thermodynamic gap.

Hypotheses

Let $s\mapsto\Phi(s)$ be differentiable for $s\in[0,1]$. The standard finite-volume-to-thermodynamic spectral-flow theorem assumes, in a typical form:

1. finite-dimensional local spin spaces;

2. a regular exhaustion $(\Lambda_n)$ with controlled geometry;

3. a decay norm for $\Phi(s)$ and $\partial_s\Phi(s)$ bounded uniformly in $s$;

4. a selected finite-volume spectral interval $I_s$;

5. a separation $\gamma>0$ between that interval and the rest of the spectrum, uniform in $s$ and $n$.

Choose a filter $W_\gamma$ adapted to the gap. The finite-volume generator is

$$D_{\Lambda_n}(s) = \int_{\mathbb R}W_\gamma(t) \tau_t^{H_{\Lambda_n}(s)} \bigl(\partial_sH_{\Lambda_n}(s)\bigr) \,dt.$$

The decay of the filter and the Lieb-Robinson estimate make this generator quasi-local.

Bulk spectral-flow variants

There are bulk formulations based on a unique selected ground state with a uniform GNS gap and suitable differentiability estimates. These avoid treating open-boundary low-energy modes as bulk gap closure. They still assume the bulk gap. They do not establish general perturbative stability.

Frustration-free reference system

Assume an interaction indexed by sites,

$$H_0=\sum_{x\in\Gamma}h_x,$$

where $h_x\geq0$ is supported in a ball $b_x(R)$ of common finite radius, $\sup_x\|h_x\|<\infty$, and the selected infinite-volume state has zero energy on every local term.

Let $H_0^{\mathrm{GNS}}$ be the positive GNS generator. A stability theorem starts with

$$\gamma_0=\operatorname{gap}(H_0^{\mathrm{GNS}})>0.$$

This is a pre-existing bulk gap, not a consequence of frustration freeness.

Local gap control

For controlled local regions $\Lambda(x,n)$, assume a polynomial lower bound on the local gap,

$$\operatorname{spec}(H_{\Lambda(x,n)}) \subset \{0\}\cup[\gamma_1n^{-\alpha},\infty)$$

for constants $\gamma_1>0$ and $\alpha\geq0$. The local gap may decay, but its decay is quantified.

Local Topological Quantum Order

Let $P_{b_x(m)}$ project onto the local ground space in a ball of radius $m$. A representative LTQO estimate is

$$\left\| P_{b_x(m)}AP_{b_x(m)} -\omega_0(A)P_{b_x(m)} \right\| \leq \|A\|(1+k)^\nu G_0(m-k)$$

for $A$ supported in $b_x(k)$ and $m\geq k$. The decay function $G_0$ must have enough finite moments relative to the spatial growth, partition growth, and local-gap exponent.

This estimate says that local ground states become indistinguishable by an observable sufficiently far from the boundary. Its quantitative form is essential to the perturbative argument.

Anchored perturbations

Write the perturbation as an anchored interaction

$$V=\sum_{x\in\Gamma}\sum_{n\geq0}\Phi(x,n), \qquad \Phi(x,n)\in\mathcal A_{b_x(n)}^{\mathrm{sa}},$$

with stretched-exponential decay

$$\|\Phi(x,n)\| \leq \|\Phi\|e^{-an^\theta}, \qquad a>0, \quad 0<\theta\leq1.$$

What the theorem does not prove

Theorem 7.1 does not apply automatically to:

• arbitrary frustrated Hamiltonians;

• power-law interactions outside the allowed decay class;

• reference systems without a known bulk gap;

• models lacking local gap control or LTQO;

• families in which the symmetry or ground-state convention changes;

• claims about all open-boundary spectra.

Hamiltonian family object

Let $S$ be a compact Hausdorff or profinite test object. Define schematically

$$\mathfrak{Ham}_F(S) = \left\{ (\Phi_s)_{s\in S}: \sup_s\|\Phi_s\|_F<\infty, \text{ with local F-continuity} \right\}.$$

Additional data records symmetry, on-site Hilbert spaces, and the allowed coarse geometry. The assignment should be treated as a groupoid or higher stack once unitary equivalences and automorphisms are included.

Gap witness

Define the quantitative witness object

$$\mathfrak{Gap}_F^{\mathrm{wit}}(S) = \left\{ (\Phi,\mathsf w): \Phi\in\mathfrak{Ham}_F(S), \ \mathsf w\text{ is a gap witness} \right\}.$$

The projection $$p_S:\mathfrak{Gap}_F^{\mathrm{wit}}(S)\longrightarrow\mathfrak{Ham}_F(S)$$ forgets the witness. It is not generally injective because one family can have many lower bounds, states, exhaustions, or theorem providers. Thus the witnessed object is a fibration of data over the Hamiltonian functor, not a subfunctor in the monomorphism sense.

Define the qualitative gapped image by propositional existence: $$\mathfrak{Gap}_F^{\mathrm{prop}}(S) = \{\Phi\in\mathfrak{Ham}_F(S):\|\exists\mathsf w,\ (\Phi,\mathsf w)\in\mathfrak{Gap}_F^{\mathrm{wit}}(S)\|\}.$$ Here $\|{-}\|$ means that only existence is retained. Equivalently, take the image of $p_S$. The qualitative object is a subfunctor of $\mathfrak{Ham}_F$ when image formation and pullback are implemented in the chosen sheaf or stack category. Both constructions are proposed.

Descent is not gap creation

Suppose a finite jointly surjective family $S_i\to S$ covers the parameter object. Compatible interaction families can descend. If every local witness comes with the same explicit lower bound and compatible state or band data, the witness can also descend in a controlled formulation.

It is invalid to assume only that every restriction has some unspecified positive lower bound. The minimum is available for a finite cover, but the selected bands and states must agree on overlaps. For varying or infinite covers, further uniformity is required. Sheaf descent organizes compatible evidence. It does not produce evidence that was not supplied.

If gapped neighborhoods form an open cover of a compact parameter space, then compactness provides a finite subcover. Compatible quantitative witnesses on that finite subcover yield a common positive minimum. This argument still requires one fixed predicate and compatible state or band conventions. A bare pointwise statement need not provide such neighborhoods or compatibility.

Openness and discriminant locus

For a norm-continuous finite matrix family with a fixed-rank isolated cluster, gappedness is open. For interacting thermodynamic families, openness follows only inside a class covered by a stability theorem.

Given a parameter map $f:B\to\mathfrak{Ham}_F$, define the witnessed gapped locus

$$U_f=B\times_{\mathfrak{Ham}_F}\mathfrak{Gap}_F^{\mathrm{prop}}$$

and the gapless discriminant

$$\Sigma_f=B\setminus U_f.$$

On underlying parameter sets or spaces, this pullback is a genuine subobject, so its complement is meaningful. The larger pullback with $\mathfrak{Gap}_F^{\mathrm{wit}}$ is instead a bundle of witnesses over $U_f$ and must not be subtracted from $B$. The notation is meaningful only after the gap predicate, image construction, and witness category are fixed. A topological phase label is expected to be locally constant on $U_f$ after quotienting by the chosen stable gapped equivalences.

Two-level constant-rank family

Let

$$H_s= \begin{pmatrix} -1 & s\\ s & 1 \end{pmatrix}, \qquad s\in[-1,1].$$

The eigenvalues are $\pm\sqrt{1+s^2}$, so the separation is $2\sqrt{1+s^2}\geq2$. The negative spectral projection has constant rank one. This is the elementary setting where compactness and continuity correctly produce a common gap.

A stable product-spin perturbation

For $N$ qubits, consider

$$H_0=\sum_{x=1}^N p_x, \qquad V=\sum_{x=1}^N v_x,$$

with $\|v_x\|\leq\epsilon$ and commuting diagonal $v_x$. If every excited on-site level remains at least $1-2\epsilon$ above the local ground level, then the many-body product gap is at least $1-2\epsilon$, independent of $N$. This direct estimate uses the product and commuting structure. It is not a general theorem for noncommuting perturbations.

Bulk and boundary conventions

An open topological chain can have boundary modes with a splitting that vanishes exponentially in length, while the periodic bulk has a stable gap. The literal open-chain ground-state gap, the open-chain ground-band gap, and the bulk GNS gap answer different questions. A phase definition intended to ignore protected edge degeneracy should use a band or bulk predicate and say so explicitly.

Lean theorem interfaces

A Lean library can honestly represent the logical dependency graph without formalizing the full analytic proofs. It should contain:

• finite sites, finite supports, and finite-volume Hamiltonian data;

• a parameter family and a predicate expressing a common norm bound;

• literal finite-spectrum gaps and selected-band gaps;

• a structure containing a positive common gap witness;

• an abstract GNS-gap predicate whose provider is an explicit interface;

• an abstract spectral-flow provider that requires a uniform gap witness;

• an abstract stability provider that lists LTQO and local-gap inputs;

• status and provenance fields for each imported analytic result.

The preferred design uses structures and theorem-provider typeclasses rather than global axioms. A concrete development can instantiate the interface when the relevant theorem has been formalized. No declaration should suggest that Lean proved an infinite-volume spectral gap merely because a finite list of eigenvalues was checked.

Haskell demonstrations

Executable code accompanying this paper checks finite calculations:

1. ordered-spectrum gap extraction;

2. selected-band separation;

3. the matrix family in theorem 4.2;

4. the $L^{-2}$ closing upper bound for the ferromagnetic chain;

5. finite prefixes of the moving weak-defect gap sequence;

6. predicates distinguishing pointwise positivity from a declared common lower bound.

These checks are computational. They catch convention and implementation errors. They are not thermodynamic proofs.

Why a numerical gap function is insufficient

Writing $\operatorname{gap}(H)$ suggests a canonical real number. In the thermodynamic setting, the notation hides choices. Which finite volumes and boundaries are used? Is a near-degenerate ground multiplet one band or several levels? Which infinite-volume state and representation are selected? Is the claim about a bulk generator or an edge spectrum? A gap witness makes these choices data rather than prose.

Why condensed mathematics still helps

The negative conclusion would be too strong if it said condensed mathematics adds nothing. It adds a coherent category for continuous and profinite families, finite-resolution disorder, symmetry objects, and descent. It can organize restrictions and gluing of an already established uniform gap witness. It can also place the gapless locus inside a parameterized moduli problem. The point is narrower: categorical organization does not replace the many-body estimate.

Relation to topological phase transitions

On a witnessed gapped region $U$, a stable phase invariant should be locally constant. A path connecting different labels must leave $U$ and meet the discriminant $\Sigma$. The local topology of $\Sigma$ may carry a relative charge when a generalized cohomology invariant is defined. This reasoning depends on the gap predicate. If pointwise but nonuniform families are admitted as single gapped objects, the phase label can fail to have the stability needed for this interpretation.

Relation to effective field theory

A low-energy field theory presupposes a controlled separation of scales. A uniform thermodynamic gap is one possible input for a topological effective description, but it does not alone construct the continuum approximation. Conversely, a field-theoretic bordism class does not prove that a microscopic Hamiltonian realizes a uniform gap. The microscopic-to-effective comparison must preserve the gap claim as a separate verified property.

Noninvertible phases

The gap predicates developed here apply to invertible and noninvertible systems. A later invertible phase spectrum captures only the sector with a stacking inverse. General topological order requires excitation and defect categories in addition to a gap witness. The analytic foundation is shared, but the classification object is larger.

Object declaration

The claim should first identify the microscopic object:

1. State the metric lattice or coarse space and its volume-growth or tail properties.

2. State the local Hilbert spaces or local observable algebras.

3. Give the interaction and its decay norm.

4. State the symmetry action and whether it is fixed along the family.

5. Distinguish a bounded observable from a formal interaction generator.

Failure at this stage means that no thermodynamic spectral predicate has yet been defined.

Spectral predicate declaration

The claim should then choose exactly one primary predicate:

1. Literal finite-volume ground-state gap.

2. Finite-volume separation above a selected low-energy band.

3. Uniform finite-volume band gap along a declared exhaustion and boundary convention.

4. Bulk GNS gap for a selected infinite-volume ground state.

5. Uniform bulk GNS gap for a parameterized family of selected states.

If more than one predicate is used, the comparison theorem must be cited with its uniqueness, regularity, exhaustion, and boundary assumptions. Similar notation is not a proof that the predicates coincide.

Quantifier audit

For a family indexed by $S$ and volumes indexed by $n$, write the quantifiers in full. The desired statement is typically

$$\exists\gamma>0\ \forall s\in S\ \forall n\geq n_0: \gamma_{s,n}\geq\gamma.$$

The weaker statement

$$\forall s\in S\ \forall n\ \exists\gamma_{s,n}>0: \gamma_{s,n}\geq\gamma_{s,n}$$

is nearly automatic for a finite matrix after exact degeneracies are grouped. It contains no common thermodynamic scale. Changing the order of these quantifiers changes the physical assertion.

Evidence ladder

Classify the available evidence at one of four levels:

The result status should match the strongest completed level.

Boundary audit

For each finite-volume statement, record:

• open, periodic, twisted, or symmetry-breaking boundary conditions;

• whether boundary terms are uniformly bounded and local;

• whether edge modes belong to the selected ground band;

• whether the claimed phase invariant is bulk, boundary, or relative;

• which comparison, if any, relates the finite system to a GNS bulk representation.

A bulk-boundary correspondence can predict protected edge behavior. It does not justify calling the open-boundary literal gap a bulk gap.

Perturbation audit

Before citing a stability theorem, verify:

1. The reference gap is already proved in the theorem’s required sense.

2. The reference interaction belongs to the theorem’s structural class.

3. Local gap or LTQO estimates have the required quantitative decay.

4. The perturbation belongs to the stated normed interaction class.

5. The perturbation strength is below a volume-independent threshold.

6. The selected symmetry and ground-state conventions are preserved.

The phrase “small local perturbation” is insufficient without a norm, threshold, and hypothesis match.