ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Gallagher correspondence for a direct product

Example

Let $N, Q$ be finite groups, $G = N \times Q$ , and identify $N$ with $N \times {1}$ . Fix $θ \in Irr (N)$ afforded by $S$ . Then $I_{G} (θ) = G$ , and $\tilde{S} (n, q) = S (n)$ extends $S$ to $G$ . The irreducible $G$ -modules above $θ$ are exactly, without repetitions, the modules $S ⊠ U$ for $U \in Irr (Q)$ , where $(n, q) (s \otimes u) = (n s) \otimes (q u) .$ Their ramification indices are $\dim U$ .

Facts & Assumptions

Given: The groups, modules, characters, and hypotheses in the example. All representations here are finite-dimensional complex left representations.

[F1]

Given an extension to inertia, tensoring it with inflated quotient irreducibles is a bijection above the type, with ramification equal to quotient degree. (Gallagher correspondence for an extendible type).

Verification

technique · direct

1.1

For $(a, b) \in N \times Q$ , conjugation sends $(n, 1)$ to $(a^{- 1} n a, 1)$ in the left-character convention. Characters are invariant under inner conjugation of $N$ by similarity of matrices, so every element fixes $θ$ and inertia is $G$ . The map $(n, q) \mapsto S (n)$ is multiplicative and restricts to the original action. The quotient map $(n, q) \mapsto q$ identifies $G / N$ with $Q$ .

givenalgebra

2.1

Gallagher applies to this extension. Its tensor with an inflated quotient module has exactly the displayed action, hence is $S ⊠ U$ . The bijection gives irreducibility, exhaustivity, and uniqueness of the parameter. Restricting to $N$ makes the second factor trivial and gives $\dim U$ copies of $S$ , which is the ramification. When $Q = 1$ this is just $S$ ; when $N = 1$ it is just $U$ .

F1step 1.1∎

Depends on

Gallagher correspondence for an extendible type

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

Britta Späth, Reduction theorems for some global-local conjectures — Theorem 1.3; tom Dieck Remark 4.2.5 specialized to a direct product (standard reference, not scraped)