ExampleConstruction: Literature-sourcedVerification: 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.

The q=2 torus boundary

Example

Assume the Axiom of Choice, used through Tits deformation. For $q = 2$ the multiplicative group $F_{2}^{\times}$ is trivial, so the diagonal torus $T ≅ (F_{2}^{\times})^{n}$ is trivial and there is exactly one character $χ = 1$ of $T$ for every $n$ : the regular case is empty for $n \geq 2$ (for $n = 1$ the unique coordinate is vacuously pairwise distinct), $W_{χ} = S_{n}$ for all $n$ , and every principal series is spherical, $I (χ) = I (1) = C [G / B]$ . The general theorems remain valid: $\dim {End}_{G} (I (1)) = ∣ S_{n} ∣ = n!$ , the constituents are indexed by partitions $λ ⊢ n$ with multiplicities $f^{λ}$ , and the finite Hecke algebra $H_{q} (n)$ at $q = 2$ is semisimple by The finite spherical Hecke algebra is semisimple with nondegenerate trace form, so Tits deformation still identifies it with $C [S_{n}]$ . Its generators also satisfy $T_{i}^{2} = T_{i} + 2$ , with distinct roots $2$ and $- 1$ . The boundary phenomenon is the collapse of the parametrising torus and of the Weyl action, not a failure of the constituent description.

Facts & Assumptions

Given: The prime power $q = 2$ , the group $G = {GL}_{n} (F_{2})$ with Borel $B$ and diagonal torus $T$ , its character group $\hat{T}$ , the Weyl group $W = S_{n}$ with its action on $\hat{T}$ , and the spherical principal series $I (1)$ .

[F1]

For $q = 2$ the group $F_{2}^{\times}$ is trivial, so $T ≅ (F_{2}^{\times})^{n}$ is trivial and $\hat{T} = {1}$ ; the Weyl action is trivial and $W_{χ} = S_{n}$ for the unique character, while the regular case consists of characters whose coordinates are pairwise distinct (Diagonal torus characters and the Weyl action).

[F2]

$I (1) ≅ C [G / B]$ , the permutation module on the complete flags (The spherical principal series is the flag permutation module).

[F3]

$\dim_{C} {End}_{G} (I (χ)) = ∣ W_{χ} ∣$ , so for the unique character this dimension is $n!$ (The Weyl stabiliser controls the principal series endomorphisms).

[F4]

The constituents of the spherical principal series are indexed by the partitions $λ ⊢ n$ with multiplicities $f^{λ}$ , the numbers of standard tableaux (The constituents of the spherical principal series of GL_n).

[F5]

The finite Hecke algebra $H_{q} (n)$ is semisimple, with quadratic relation $T_{s_{i}}^{2} = (q - 1) T_{s_{i}} + q 1$ ; at $q = 2$ this is $T_{s_{i}}^{2} = T_{s_{i}} + 2$ , whose two roots $2$ and $- 1$ are distinct (The finite spherical Hecke algebra is semisimple with nondegenerate trace form, The rank-one quadratic relation in the finite Hecke algebra).

[F6]

Assume AC; Tits deformation identifies $H_{q} (n)$ with $C [S_{n}]$ for every prime power $q$ , hence also for $q = 2$ (The finite Hecke algebra is non-canonically isomorphic to the group algebra of S_n, The Axiom of Choice).

Verification

technique · direct

1.1F1F2

For $q = 2$ the group $F_{2}^{\times} = {1}$ is trivial, so the diagonal torus $T ≅ (F_{2}^{\times})^{n}$ is the trivial group and its character group has the single element $1$ ; the Weyl action fixes it, so $W_{1} = S_{n}$ , and every principal series is $I (1)$ . A regular character would need pairwise distinct coordinates, impossible in a one-element group when $n \geq 2$ ; for $n = 1$ the single coordinate is vacuously pairwise distinct.

1.2F3F4

Since the unique character is fixed by $W$ , [F3] gives $\dim_{C} {End}_{G} (I (1)) = n!$ , and [F4] gives the constituent indexing by partitions with multiplicities $f^{λ}$ .

1.3F5F6

By [F5] the Hecke algebra is semisimple with quadratic relation $T_{s_{i}}^{2} = T_{s_{i}} + 2$ at $q = 2$ , and the two roots $2 \neq - 1$ are distinct; by [F6] Tits deformation identifies it with $C [S_{n}]$ in this case as in every other. Hence the collapse of $\hat{T}$ to a point and of the Weyl action to the trivial action is a genuine boundary phenomenon of the parametrising torus, while the endomorphism algebra, the constituent multiplicities and the Tits isomorphism retain their general form.

2.1F1F2F3F4F5F6∎

Steps 1.1-1.3 establish the two boundary statements: the torus and the regular characters collapse, whereas the endomorphism algebra, the partition parametrisation with multiplicities $f^{λ}$ and the Tits isomorphism to $C [S_{n}]$ remain valid. AC is carried only from the Tits-deformation supplier [F6], as declared.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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

Ivan Losev, Lecture 8: Representations of GL_n(F_q) - Sections 2.1 and 2.3 (the spherical case and Tits deformation), PDF pp. 3-5 (standard reference, not scraped)
Jay Taylor, Finite Reductive Groups - Theorem 5.18 and Example 5.22, printed pp. 45-46 (standard reference, not scraped)
Olivier Dudas and Jean Michel, Lectures on Finite Reductive Groups and Their Representations - Section 11.1 and Remark 11.6, printed pp. 45-47 (standard reference, not scraped)