ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Matrix coefficients of the standard SU(2) representation

Example

Assume the Axiom of Choice. Write an element of $S U (2)$ as $g = (\begin{array}{cc} a & b \\ - \overline{b} & \overline{a} \end{array})$ with $∣ a ∣^{2} + ∣ b ∣^{2} = 1$ . Then the four coordinate functions $a, b, - \overline{b}, \overline{a}$ are the matrix coefficients of the standard two-dimensional representation in the standard orthonormal basis, and they are pairwise orthogonal in $L^{2} (S U (2))$ with squared norm $\frac{1}{2}$ .

Facts & Assumptions

Given: Assume the Axiom of Choice; the standard representation of $S U (2)$ on $C^{2}$ with orthonormal basis $e_{1}, e_{2}$ and normalized Haar measure.

[L1]

Matrix coefficients are $π_{i j} (g) = ⟨ π (g) e_{j}, e_{i} ⟩$ for an orthonormal basis (Matrix coefficients and characters).

[L2]

Schur orthogonality: for an irreducible unitary representation of dimension $d$ , $\int_{G} π_{i j} (g) \overline{π_{k l} (g)} d g = δ_{i k} δ_{j l} / d$ (Schur orthogonality).

Verification

technique · direct

1.1

With $g e_{1} = (a, - \overline{b})$ and $g e_{2} = (b, \overline{a})$ , the matrix coefficients in the standard basis are $π_{11} = a$ , $π_{21} = - \overline{b}$ , $π_{12} = b$ and $π_{22} = \overline{a}$ , by [L1]; these are exactly the four displayed coordinate functions.

2.1

The standard representation is irreducible. Indeed, for every unit vector $(u, v) \in C^{2}$ , the matrix $(\begin{array}{cc} u & - \overline{v} \\ v & \overline{u} \end{array})$ lies in $S U (2)$ and sends $e_{1}$ to $(u, v)$ ; hence $S U (2)$ acts transitively on the unit sphere. Any nonzero invariant subspace therefore contains the whole unit sphere and equals $C^{2}$ . Since the representation has dimension two, [L2] applies with $d = 2$ : $\int_{S U (2)} π_{i j} \overline{π_{k l}} d g = δ_{i k} δ_{j l} / 2$ .

L2step 1.1algebra

3.1

Reading off the four cases gives that each of $a, b, - \overline{b}, \overline{a}$ has squared norm $\frac{1}{2}$ and that distinct coordinate functions are orthogonal, which is the assertion.

L2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

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

Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)