ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge 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 rank-two Jones–Wenzl idempotent at loop value two

Example

Let $q = 1$ , so $δ = 2$ and $[r]_{q} = r$ . In rank two the recursion gives $p_{2} = 1 - \frac{1}{2} d_{1}$ , an idempotent annihilated by $d_{1}$ , with normalized closure trace $τ_{2} (p_{2}) = 3 / 4$ .

Facts & Assumptions

Given: $q = 1$ , $δ = 2$ , $[r]_{q} = r$ , and the rank-two generator $d_{1}$ .

[F1]

$d_{1}^{2} = 2 d_{1}$ , and $τ_{2} (1) = 1$ , $τ_{2} (d_{1}) = 1 / 2$ (The elementary diagram generators satisfy the local Temperley–Lieb relations, Normalized Temperley–Lieb trace from diagram closure, The normalized closure trace is cyclic and satisfies the Markov rules).

[F2]

The recursion is $p_{2} = 1 - \frac{[1]}{[2]} d_{1}$ , and its trace formula is $τ_{2} (p_{2}) = [3] / 2^{2}$ (Jones–Wenzl recursion in the nonvanishing-denominator range, The Jones–Wenzl recursion gives annihilating idempotents and their trace).

Verification

Given: The stated parameter and rank-two algebra.

1.1F1F2givenalgebra

Since $[1] = 1$ and $[2] = 2$ , the recursion gives $p_{2} = 1 - \frac{1}{2} d_{1}$ . By [F1], $p_{2}^{2} = 1 - d_{1} + \frac{1}{4} d_{1}^{2} = 1 - \frac{1}{2} d_{1} = p_{2}, d_{1} p_{2} = p_{2} d_{1} = 0.$ The identity coefficient is $1$ , so $p_{2} \neq 0$ .

2.1F1F2step 1.1∎

The trace formula in [F2] gives $τ_{2} (p_{2}) = [3] / 2^{2} = 3 / 4$ . This calculation uses the closure trace normalization $τ_{2} (1) = 1$ , not the unnormalized categorical trace.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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)