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.

The two-strand Jones-Wenzl projector at loop value two

Example

Take $R = C$ , $δ = 2$ , so $[1] = 1$ , $[2] = 2$ , and $[3] = 3$ . The recursion gives

$p_{2} = 1_{2} - \frac{1}{2} U_{1} .$

It is a nonzero idempotent annihilated by $U_{1}$ on both sides, has partial trace $\frac{3}{2} p_{1}$ , and has unnormalized closure trace $3$ .

Facts & Assumptions

Given: The two-strand Temperley–Lieb algebra with $U_{1}^{2} = 2 U_{1}$ .

[F1]

The recursion is $p_{2} = 1_{2} - ([1] / [2]) U_{1}$ when $[2]$ is a unit (Jones–Wenzl recursion over unit quantum integers).

[F2]

For unit quantum integers the projector is idempotent, annihilates the generator, and has partial trace $([3] / [2]) p_{1}$ and closure trace $[3]$ (Jones–Wenzl projectors: annihilation, uniqueness, partial trace, and closure).

[F3]

The recurrence gives $[2] = δ$ and $[3] = δ [2] - [1]$ (Temperley–Lieb quantum integers and quantum characteristic).

Verification

technique · direct calculation

1.1F1F3givenalgebra

Substituting $δ = 2$ into [F3] yields $[2] = 2$ and $[3] = 2 \cdot 2 - 1 = 3$ . Thus [F1] gives $p_{2} = 1_{2} - \frac{1}{2} U_{1}$ ; the coefficient denominator is a unit in $C$ .

2.1F1step 1.1algebra

Directly, $p_{2}^{2} = 1 - U_{1} + \frac{1}{4} U_{1}^{2} = 1 - U_{1} + \frac{1}{2} U_{1} = p_{2}$ and $U_{1} p_{2} = p_{2} U_{1} = U_{1} - \frac{1}{2} (2 U_{1}) = 0$ . The identity and cup-cap diagrams are distinct basis vectors, so the coefficient $1$ on the identity makes $p_{2} \neq 0$ .

3.1F2F3step 1.1algebra∎

From [F2], ${ptr}_{2} (p_{2}) = ([3] / [2]) p_{1} = \frac{3}{2} p_{1}$ and ${Tr}_{2} (p_{2}) = [3] = 3$ . These agree with direct closure: ${Tr}_{2} (1_{2}) = 4$ and ${Tr}_{2} (U_{1}) = 2$ , so $4 - \frac{1}{2} (2) = 3$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

Joshua Chen, The Temperley-Lieb Categories and Skein Modules (standard reference, not scraped)
K. Iohara, G. I. Lehrer, and R. B. Zhang, The Jones Quotients of the Temperley-Lieb Algebras (standard reference, not scraped)