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.

Unitriangular global basis elements at small rank

Example

At $e = 2$ the ambient lower basis in degrees $\leq 3$ is $\emptyset \mapsto ∣ \emptyset ⟩$ , $1 \mapsto ∣ 1 ⟩$ , $11 \mapsto ∣ 11 ⟩$ , $2 \mapsto ∣ 2 ⟩ + q ∣ 11 ⟩$ , $111 \mapsto ∣ 111 ⟩$ , $3 \mapsto ∣ 3 ⟩ + q ∣ 111 ⟩$ , $21 \mapsto ∣ 21 ⟩$ . The basic labels in these degrees are $\emptyset, 1, 2, 3, 21$ (not $11$ or $111$ ). In degree $4$ , rows and columns ordered $4, 31, 22, 211, 1111$ , the full lower transition matrix $D$ (column $= G$ -label, row $=$ standard shape) is

$(\begin{array}{ccccc} 1 & 0 & 0 & 0 & 0 \\ q & 1 & 0 & 0 & 0 \\ 0 & q & 1 & 0 & 0 \\ q & q^{2} & q & 1 & 0 \\ q^{2} & 0 & 0 & q & 1 \end{array}) .$

Its basic columns are $4$ and $31$ . All entries lie in $Z [q]$ , the diagonal is $1$ , and off-diagonal entries lie in $q Z [q]$ , with the proved dominance and core bounds. The apparent transpose-conjugation identity holds accidentally for the displayed degrees $\leq 3$ but is false generally: $d_{(211), (4)} = q$ whereas $d_{(1111), (31)} = 0$ . The source symmetry concerns the bar transition matrix, not $D$ . The ambient bar-fixed $G (111)$ lies outside the basic module; no arbitrary bar-fixed combination need lie in one isotypic summand.

Facts & Assumptions

Given: The $e = 2$ partition Fock space with its lower global basis, dominance order, and the node actions of the small shapes.

[F1]

The lower global basis is dominance-unitriangular with $q Z [q]$ off-diagonal coefficients, same-core support and diagonal $1$ ; the regular labels are the lower global basis of $M$ (The basic representation global basis is unitriangular in the partition basis).

[F2]

Dominance is the prefix-sum order, conjugation reverses it, and the regular labels are those with part multiplicities $< 2$ (Dominance order on partitions, The regular-partition label convention and the Mullineux crystal involution).

[F3]

The ordinary node actions on shapes of size $\leq 3$ are the $e = 2$ table of Node actions for partitions of size at most three.

Verification

1.1F1F2F3algebra

The degrees $\leq 3$ . Solving the triangular bar equations degree by degree with the reversal bar: in degree $2$ the only correction of $2$ is $q 11$ ; in degree $3$ the partition $21$ is the only shape whose residue multiset forces no correction and $3$ receives the correction $q 111$ ; the remaining shapes are bar-fixed. This gives the displayed degree- $\leq 3$ elements, and the basic labels are the $2$ -regular ones, namely $\emptyset, 1, 2, 3, 21$ , with $11$ and $111$ non-regular.

2.1step 1.1F1F2algebra

The degree-four bar calculation. The finite reversal formula of [F1], at any cutoff longer than four, and straightening give $ψ ∣ 4 ⟩ = ∣ 4 ⟩ + (q - q^{- 1}) ∣ 31 ⟩ + (q^{- 2} - 1) ∣ 22 ⟩ + (q^{2} - 1) ∣ 1111 ⟩$ , $ψ ∣ 31 ⟩ = ∣ 31 ⟩ + (q - q^{- 1}) ∣ 22 ⟩ + (q^{2} - 1) ∣ 211 ⟩$ , $ψ ∣ 22 ⟩ = ∣ 22 ⟩ + (q - q^{- 1}) ∣ 211 ⟩ + (q^{- 2} - 1) ∣ 1111 ⟩$ , $ψ ∣ 211 ⟩ = ∣ 211 ⟩ + (q - q^{- 1}) ∣ 1111 ⟩$ and $ψ ∣ 1111 ⟩ = ∣ 1111 ⟩$ . Substituting these five formulas, with coefficient bar, verifies the displayed columns $G (4) = ∣ 4 ⟩ + q ∣ 31 ⟩ + q ∣ 211 ⟩ + q^{2} ∣ 1111 ⟩$ , $G (31) = ∣ 31 ⟩ + q ∣ 22 ⟩ + q^{2} ∣ 211 ⟩$ , $G (22) = ∣ 22 ⟩ + q ∣ 211 ⟩$ , $G (211) = ∣ 211 ⟩ + q ∣ 1111 ⟩$ and $G (1111) = ∣ 1111 ⟩$ : each is bar fixed with its stated leading residue and coefficients in $q Z [q]$ . Uniqueness in [F1] therefore identifies them with the lower lifts. The basic labels are the regular shapes $4, 31$ , and the nonzero positions visibly respect dominance.

3.1step 2.1F2algebra

The false transpose symmetry. Conjugation of partitions sends $211 \mapsto 31$ and $4 \mapsto 1111$ , so the transpose-conjugation equality would require $d_{(211), (4)} = d_{(1111), (31)}$ ; but the degree- $4$ matrix gives $d_{(211), (4)} = q$ and $d_{(1111), (31)} = 0$ . Hence the equality fails in general; the source's symmetry statement concerns the bar transition matrix $A$ , not the lower matrix $D$ .

4.1step 1.1step 2.1step 3.1∎

Conclusion. The displayed elements are the actual lower global basis elements in degrees $\leq 4$ , their coefficients are integral and dominance-triangular, the basic columns are the regular labels, and the naive transpose symmetry of $D$ is refuted by the explicit pair.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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