ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Node actions for partitions of size at most three

Example

For charge $0$ the following tables give all $E_{i}, F_{i}$ actions on the standard partition vectors of size $\leq 3$ (outputs of size $4$ included) and all Cartan exponents $N_{i} = # {addable}_{i} - # {removable}_{i}$ . A shape denotes its standard vector; omitted terms have coefficient $0$ . Entries are ordered $i = 0, \dots, e - 1$ .

$e = 2$ :

shape	$N$	$F$	$E$
$\emptyset$	$(1, 0)$	$((1), 0)$	$(0, 0)$
$(1)$	$(- 1, 2)$	$(0, (2) + q (1, 1))$	$(\emptyset, 0)$
$(2)$	$(1, 0)$	$((3), q^{- 1} (2, 1))$	$(0, q^{- 1} (1))$
$(1, 1)$	$(1, 0)$	$((1, 1, 1), (2, 1))$	$(0, (1))$
$(3)$	$(- 1, 2)$	$(0, (4) + q (3, 1))$	$((2), 0)$
$(2, 1)$	$(3, - 2)$	$((3, 1) + q (2, 2) + q^{2} (2, 1, 1), 0)$	$(0, (2) + q (1, 1))$
$(1, 1, 1)$	$(- 1, 2)$	$(0, (2, 1, 1) + q (1, 1, 1, 1))$	$((1, 1), 0)$

$e = 3$ :

shape	$N$	$F$	$E$
$\emptyset$	$(1, 0, 0)$	$((1), 0, 0)$	$(0, 0, 0)$
$(1)$	$(- 1, 1, 1)$	$(0, (2), (1, 1))$	$(\emptyset, 0, 0)$
$(2)$	$(0, - 1, 2)$	$(0, 0, (3) + q (2, 1))$	$(0, (1), 0)$
$(1, 1)$	$(0, 2, - 1)$	$(0, (2, 1) + q (1, 1, 1), 0)$	$(0, 0, (1))$
$(3)$	$(1, 0, 0)$	$((4), 0, q^{- 1} (3, 1))$	$(0, 0, q^{- 1} (2))$
$(2, 1)$	$(1, 0, 0)$	$((2, 2), q^{- 1} (2, 1, 1), (3, 1))$	$(0, q^{- 1} (1, 1), (2))$
$(1, 1, 1)$	$(1, 0, 0)$	$((1, 1, 1, 1), (2, 1, 1), 0)$	$(0, (1, 1), 0)$

In both tables $\sum_{i} N_{i} = 1$ and $K_{i}$ acts by $q^{N_{i}}$ , so the central product acts by $q$ . The normalized crystal arrows on the same residues are computed separately by signature reduction; a minimal exponent of ordinary $F$ is not their definition. The source calibration is Leclerc Exercise 15 at $e = 2$ : $F_{0} ∣ 3, 1 ⟩ = q^{- 1} ∣ 3, 2 ⟩ + ∣ 3, 1, 1 ⟩$ and $E_{0} ∣ 3, 1 ⟩ = q^{- 2} ∣ 2, 1 ⟩$ .

Facts & Assumptions

Given: The charge- $0$ partition Fock space with its node formulas and the content order, and all partitions of size $\leq 3$ .

[F1]

$F_{i} ∣ λ ⟩ = \sum_{γ} q^{N_{i}^{r} (λ, γ)} ∣ λ + γ ⟩$ over addable $i$ -nodes $γ$ , and $E_{i} ∣ μ ⟩ = \sum_{γ} q^{- N_{i}^{l} (μ - γ, μ)} ∣ μ - γ ⟩$ over removable $i$ -nodes, with the signed counts of The node order and the signed exponents $N_{i}^{l}$ and $N_{i}^{r}$ ; the counts are taken in the smaller diagram (Semi-infinite wedges are indexed by partitions and the action gives the node formulas).

[F2]

Addable nodes are $(r, λ_{r} + 1)$ with $r = 1$ or $λ_{r - 1} > λ_{r}$ ; removable nodes are $(r, λ_{r})$ with $λ_{r} > λ_{r + 1}$ ; the residue is $c - r m o d e$ (Removable and addable nodes, The level-one partition Fock space and node residues).

[F3]

$N_{i} (λ) = # {addable}_{i} - # {removable}_{i}$ and $\sum_{i} N_{i} = 1$ (The addable-minus-removable node count is the level-one Cartan pairing).

Verification

1.1F1F2givenalgebra

Every listed entry is a direct finite evaluation of [F1] on the partitions of size $\leq 3$ . For $e = 2$ : at $(1)$ the addable $1$ -nodes are $(1, 2)$ (content $1$ ) and $(2, 1)$ (content $- 1$ ), with signed counts $0$ and $1$ , giving $F_{1} ∣ 1 ⟩ = ∣ 2 ⟩ + q ∣ 1, 1 ⟩$ and $N = (- 1, 2)$ ; at $(2)$ the $0$ -addable cell $(1, 3)$ has exponent $0$ and the $1$ -addable cell $(2, 1)$ has signed count $- 1$ , giving $F_{0} ∣ 2 ⟩ = ∣ 3 ⟩$ , $F_{1} ∣ 2 ⟩ = q^{- 1} ∣ 2, 1 ⟩$ , $E_{1} ∣ 2 ⟩ = q^{- 1} ∣ 1 ⟩$ ; at $(2, 1)$ the three $0$ -addable cells $(1, 3), (2, 2), (3, 1)$ have signed counts $0, 1, 2$ , giving $F_{0} ∣ 2, 1 ⟩ = ∣ 3, 1 ⟩ + q ∣ 2, 2 ⟩ + q^{2} ∣ 2, 1, 1 ⟩$ , while the two $1$ -removable-node computations give $E_{1} ∣ 2, 1 ⟩ = ∣ 2 ⟩ + q ∣ 1, 1 ⟩$ and $N = (3, - 2)$ ; at $(3)$ the node $(4)$ has count $0$ and $(3, 1)$ count $1$ , giving $F_{1} ∣ 3 ⟩ = ∣ 4 ⟩ + q ∣ 3, 1 ⟩$ ; at $(1, 1, 1)$ the signed counts $0$ and $1$ give $F_{1} ∣ 1, 1, 1 ⟩ = ∣ 2, 1, 1 ⟩ + q ∣ 1, 1, 1, 1 ⟩$ ; the empty and $(1, 1)$ rows are immediate.

1.2F1F2givenalgebra

The $e = 3$ table is evaluated the same way: at $(2)$ the $2$ -addable nodes $(3)$ and $(2, 1)$ have counts $0$ and $1$ , so $F_{2} ∣ 2 ⟩ = ∣ 3 ⟩ + q ∣ 2, 1 ⟩$ , and $E_{1} ∣ 2 ⟩ = ∣ 1 ⟩$ ; at $(1, 1)$ the $1$ -addable nodes give $F_{1} ∣ 1, 1 ⟩ = ∣ 2, 1 ⟩ + q ∣ 1, 1, 1 ⟩$ and $E_{2} ∣ 1, 1 ⟩ = ∣ 1 ⟩$ ; at $(3)$ the $2$ -addable node $(3, 1)$ has count $- 1$ and $E_{2} ∣ 3 ⟩ = q^{- 1} ∣ 2 ⟩$ ; at $(2, 1)$ the counts give $F_{0} ∣ 2, 1 ⟩ = ∣ 2, 2 ⟩$ , $F_{1} ∣ 2, 1 ⟩ = q^{- 1} ∣ 2, 1, 1 ⟩$ , $F_{2} ∣ 2, 1 ⟩ = ∣ 3, 1 ⟩$ and $E_{1} ∣ 2, 1 ⟩ = q^{- 1} ∣ 1, 1 ⟩$ , $E_{2} ∣ 2, 1 ⟩ = ∣ 2 ⟩$ ; at $(1, 1, 1)$ one gets $F_{0} ∣ 1, 1, 1 ⟩ = ∣ 1, 1, 1, 1 ⟩$ , $F_{1} ∣ 1, 1, 1 ⟩ = ∣ 2, 1, 1 ⟩$ .

2.1step 1.1F1F3algebra

Cartan exponents and Calibration. The $N$ columns are computed from the addable/removable counts and satisfy $\sum_{i} N_{i} = 1$ by [F3]; the $e = 2$ entries at $(3, 1)$ reproduce the source calibration $F_{0} ∣ 3, 1 ⟩ = q^{- 1} ∣ 3, 2 ⟩ + ∣ 3, 1, 1 ⟩$ , $E_{0} ∣ 3, 1 ⟩ = q^{- 2} ∣ 2, 1 ⟩$ when evaluated by the same formulas on the size- $4$ shape $(3, 1)$ (its addable/removable data is used in both calibration formulas and lies outside the displayed size- $\leq 3$ table).

3.1step 1.1step 1.2step 2.1∎

Conclusion. The tables list all ordinary $E_{i}, F_{i}$ actions on all standard vectors of size $\leq 3$ for $e = 2, 3$ with their Cartan exponents, they are derived from the node formulas rather than copied from a printed table, and the normalized crystal arrows on the same residues are computed separately by signature reduction.

Depends on

Used by

Dependency tree · two levels

15 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

Bernard Leclerc, Fock space representations (complete author-hosted 38-page body) (standard reference, not scraped)
Bernard Leclerc and Jean-Yves Thibon, Canonical bases of q-deformed Fock spaces, arXiv:q-alg/9602025 (standard reference, not scraped)
Matthew Fayers, Partition models for the crystal of the basic $U_q(\mathfrak{sl}_n)$-module, arXiv:0906.4129 (standard reference, not scraped)