Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-09-26 (gpt-6-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 decomposition matrix of S3 in characteristic two

Example

For S3 in characteristic 2, with ordinary irreducibles ordered as (1,sgn⁡,std⁡) and irreducible Brauer characters ordered as (φtriv,φstd), the decomposition matrix is

(101001).

Facts & Assumptions

Given: The ordinary trivial, sign, and standard characters of S3 in characteristic 2.

[F1]

The decomposition matrix is defined by the expansions of the restricted ordinary characters in the irreducible Brauer basis (Decomposition numbers and the decomposition matrix).

[F2]

The decomposition map records those modular reductions (Decomposition map from ordinary to modular Grothendieck groups).

[L1]

The 2-regular classes of S3 are represented by 1 and (123) (The p-regular classes of S3).

[L2]

The irreducible Brauer characters form a basis of the class functions on the 2-regular classes (Irreducible Brauer characters form a basis of the p-regular class functions).

Verification

technique · direct
1.1L1givenalgebra

By [L1], only the values at 1 and (123) matter. The ordinary trivial and sign characters both restrict to (1,1) on those classes, because a 3-cycle is even. The ordinary standard character restricts to (2,−1).

2.1F1F2L1L2step 1.1algebra

Let k be an algebraic closure of F2 and let W={(x1,x2,x3)∈k3:x1+x2+x3=0} with the permutation action of S3. It is the reduction of the integral sum-zero lattice for the ordinary standard representation. A 3-cycle acts on W with the two distinct nontrivial cubic-root eigenvalues; a transposition interchanges their eigenlines. Thus no line in W is S3-invariant, so W is simple. By [F2] its Brauer character is the restricted ordinary standard character (2,−1), while the trivial module gives (1,1). These two characters are independent on the two 2-regular classes, so [L2] shows that they are the full irreducible Brauer basis. Consequently [F1] writes the restricted ordinary characters as 10=φtriv,sgn⁡0=φtriv,std⁡0=φstd.

3.1step 2.1∎

Reading off the coefficients yields the displayed decomposition matrix.

Depends on

Used by

Dependency tree · two levels

12 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