ExampleConstruction: AI-generatedVerification: 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.

The rank-one level-two cyclotomic quotient

Example

Let $F$ be a field, let $q, a, b \in F^{\times}$ , and take level $r = 2$ and rank $n = 1$ with cyclotomic parameters $u_{1} = a, u_{2} = b$ . The algebra is $F [X^{\pm 1}] / ((X - a) (X - b))$ , has basis $1, X$ , and satisfies

$X^{2} = (a + b) X - a b, X^{- 1} = \frac{a + b - X}{a b} .$

Facts & Assumptions

Given: A field $F$ , units $q, a, b \in F^{\times}$ , and the rank-one level-two multiplicative presentation.

[F1]

The multiplicative cyclotomic Hecke algebra: the rank-one presentation uses an invertible generator $X$ .

[F2]

The multiplicative cyclotomic Hecke algebra: the rank-one quotient imposes $p (X) = \prod_{a} (X - u_{a}) = 0$ .

[F3]

The rank-one cyclotomic quotient has a monic basis: for rank one, $1, X, \dots, X^{r - 1}$ is a basis of the quotient by $p (X)$ .

Verification

Given: $r = 2$ , $n = 1$ , $u_{1} = a$ , and $u_{2} = b$ as in the example.

1.1F1F2algebra

Here $p (X) = X^{2} - (a + b) X + a b$ by [F2]. The equation $p (X) = 0$ gives $X^{2} = (a + b) X - a b$ . Multiplying $p (X) = 0$ by the unit $X^{- 1}$ from [F1] gives $X - (a + b) + a b X^{- 1} = 0$ , hence $X^{- 1} = (a + b - X) / (a b)$ .

2.1F3step 1.1∎

The rank-one basis lemma [F3] with $r = 2$ gives exactly the two basis vectors $1, X$ , so the displayed quotient and formulas have the claimed rank and normal form.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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.