Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedPipeline-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.

A toric logical string has constant energy barrier

Statement

If Je≤Jm, the horizontal logical string Zˉ1 has BL(Zˉ1)≤4Je. If Jm<Je, the dual horizontal logical string Xˉ2 has BL(Xˉ2)≤4Jm. In either case a noncontractible logical loop of the cheaper species has barrier at most 4min⁡(Je,Jm), independently of L.

Facts & Assumptions

Given: L≥3, fixed Je,Jm>0, the finite toric Hamiltonian, and the specified logical loops.

[F1]

Pauli-path energy barrier: the barrier is the minimum peak energy excess over all paths of single-edge Pauli errors ending at the specified logical operator.

[F2]

Exact finite-volume toric-code gap: the ground energy is Eg=−L2(Je+Jm).

[F3]

Open toric strings have endpoint syndromes: an edge-simple open primal Z trail or dual X trail has the respective defects at exactly its two endpoints; a closed such trail has no defects.

[F4]

Noncontractible toric logical loops: Zˉ1 is the horizontal primal loop with edges hi,0, and Xˉ2 is the dual horizontal loop with crossed edges vi,0.

[F5]

Finite toric-code Hamiltonian: HL is the finite sum of star terms −JeAi,j and plaquette terms −JmBi,j.

Proof

1.1givenF1F2F3F4F5constructalgebra

Suppose Je≤Jm. Apply Zh0,0,Zh1,0,…,ZhL−1,0 in that order. After k factors with 1≤k<L, the partial string is a primal trail from q0,0 to qk,0; these endpoints are distinct, so [F3] gives exactly two e defects and no m defects. By [F5], changing one star eigenvalue from +1 to −1 changes its energy contribution from −Je to +Je, an increase of 2Je; the excess is therefore 4Je. After the last factor the path is closed and has zero syndrome by [F3]. This is an elementary path in [F1] whose peak excess is at most 4Je.

1.2givenF1F2F3F4F5constructalgebra

Suppose Jm<Je. Apply Xv0,0,Xv1,0,…,XvL−1,0 in that order. The crossed dual edges form a closed horizontal dual loop. After k factors with 1≤k<L, the dual trail has distinct endpoint faces fL−1,0 and fk−1,0; [F3] gives exactly two m defects and no e defects. By [F5], each m defect raises the energy by 2Jm, so the excess is 4Jm. The final closed trail has zero syndrome by [F3] and ends at Xˉ2. This is an elementary path in [F1] with peak excess at most 4Jm.

2.1step 1.1step 1.2algebra∎

If Je≤Jm, step 1.1 gives 4Je=4min⁡(Je,Jm). If Jm<Je, step 1.2 gives 4Jm=4min⁡(Je,Jm). The bound is independent of L.

Depends on

Used by

Dependency tree · two levels

16 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