Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

Two-level avoided crossing

Statement

Consider H(s)=(s−1/2)Z+X/2 on C2, where X=(0110) and Z=(100−1). Compute its full ground-to-excited gap, derivative bounds, and rank-one JRS error bound.

Facts & Assumptions

Given: The finite path and rank-one JRS estimate from Finite adiabatic path model and Finite JRS adiabatic projector bound.

[F2]

For a rank-one band, the JRS bound is A1(1)=1T(∥H′(0)∥g(0)2+∥H′(1)∥g(1)2+∫01(∥H′′(s)∥g(s)2+7∥H′(s)∥2g(s)3)ds) (Finite JRS adiabatic projector bound).

Proof

1.1givenF1algebra

Put x=s−1/2. Direct multiplication gives H(s)2=(x2+1/4)I, so its eigenvalues are ±x2+1/4. The ground-to-excited gap is therefore g(s)=2x2+1/4, whose minimum is 1 at s=1/2 and whose endpoint values are 2. The ground band is uniformly isolated and has rank one.

1.2givenalgebra

Differentiating gives H′(s)=Z and H′′(s)=0. Since Z∗Z=I, ∥H′(s)∥=1 for every s.

2.1F2step 1.1step 1.2algebra

Substituting the endpoint values and derivatives from steps 1.1–1.2 into [F2] gives endpoint contribution 1/2+1/2=1. For the integral, with x=s−1/2, ∫017g(s)3 ds=78∫−1/21/2dx(x2+1/4)3/2=72, using the antiderivative x/((1/4)x2+1/4). Hence A1(1)=(1+7/2)/T.

3.1F2step 2.1algebra∎

The JRS conclusion consequently bounds the projector deviation by (1+7/2)/T and the transition probability out of the ground band by its square. For example, any T≥4(1+7/2)/ε makes the projector deviation at most ε/4.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources