ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

The Q = 2, 3, 4 Potts chains use three distinct q normalizations

Statement

For $Q = 2, 3, 4$ , the loop values and corresponding parameters are respectively $(δ, q) = (\sqrt{2}, e^{i π / 4})$ , $(\sqrt{3}, e^{i π / 6})$ , and $(2, 1)$ . On each site the odd generator is $\sqrt{Q} ∣ + ⟩ ⟨ + ∣$ ; on adjacent sites the even generator is $\sqrt{Q} \sum_{a = 0}^{Q - 1} ∣ a a ⟩ ⟨ a a ∣$ . For $L$ Potts sites the open Hamiltonian contains exactly $L + (L - 1) = 2 L - 1$ generators.

Facts & Assumptions

Given: The clock and shift matrices and the generator formulas from Open Potts clock-shift Temperley–Lieb generators.

[F1]

$M_{Q}^{Q} = R_{Q}^{Q} = I$ ; the displayed odd and even generators use one odd term per site and one even term per neighboring pair. (Open Potts clock-shift Temperley–Lieb generators)

[F2]

These generators satisfy the Temperley–Lieb square, adjacent triple and distant commutation relations at loop value $\sqrt{Q}$ . (The Q = 2, 3, 4 open Potts matrices satisfy Temperley–Lieb)

Proof

Given: $Q \in {2, 3, 4}$ and $L \geq 1$ .

1.1F1givenalgebra

The geometric sum $Q^{- 1} \sum_{r} M_{Q}^{r}$ is the rank-one projection onto $∣ + ⟩ = Q^{- 1 / 2} \sum_{a} ∣ a ⟩$ , and $Q^{- 1} \sum_{r} R_{1}^{r} R_{2}^{- r} = \sum_{a} ∣ a a ⟩ ⟨ a a ∣$ . Multiplying these projections by $\sqrt{Q}$ gives the stated explicit generators. From the assigned $q$ values, $q + q^{- 1} = 2 \cos (π / 4) = \sqrt{2}$ , $2 \cos (π / 6) = \sqrt{3}$ , and $2 \cos 0 = 2$ .

2.1F1F2step 1.1algebra∎

There are $L$ odd indices $2 j - 1$ for $1 \leq j \leq L$ and $L - 1$ even indices $2 j$ for $1 \leq j < L$ . Their total is $2 L - 1$ , with no additional term at the boundary. The relation verification is [F2], so each listed case has the declared open-chain Temperley–Lieb normalization.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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

A. Nichols, The Temperley-Lieb Algebra and its Generalizations in the Potts and XXZ Models (standard reference, not scraped)