CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

A transitive action need not be Frobenius

Statement refuted

Let $S_{4}$ be the symmetric group on the four letters $0, 1, 2, 3$ (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation), acting on ${0, 1, 2, 3}$ naturally, and let $H : = {σ \in S_{4} : σ (2) = 2}$ be the stabilizer of the letter $2$ (The orbit $G \cdot x$ and stabilizer $G_{x}$ of a point in a group action, Left group actions, transitive actions, and faithful actions). Then the action is transitive and nonregular, but it is not a Frobenius action: $H$ is not a Frobenius complement of $S_{4}$ (Frobenius complement and frobenius group). Explicitly:

the transposition $(0 1)$ fixes the two letters $2$ and $3$ , so some nonidentity element fixes more than one point;
for $g = (2 3) \notin H$ the stabilizer $g H g^{- 1}$ of the letter $3$ meets $H$ in ${id, (0 1)} \neq {id}$ .

Facts & Assumptions

Given: The symmetric group $S_{4} = Sym ({0, 1, 2, 3})$ , its natural action on ${0, 1, 2, 3}$ , and $H = {σ \in S_{4} : σ (2) = 2}$ .

[F1]

Cycle notation: a transposition $(a b)$ exchanges $a$ and $b$ and fixes every other letter; $(a b)^{2} = id$ ; and a permutation of the four letters fixing two of them is determined by what it does to the remaining two, so the permutations fixing both $2$ and $3$ are exactly $id$ and $(0 1)$ (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation).

[F2]

Stabilizers, cosets and conjugation: for a group $G$ acting on a set $X$ and $x \in X$ , the stabilizer $G_{x} = {g : g \cdot x = x}$ is a subgroup; point stabilizers of points in one orbit are conjugate: for $g \in G$ one has $g G_{x} g^{- 1} = G_{g \cdot x}$ , because $g σ g^{- 1}$ fixes $g \cdot x$ exactly when $σ$ fixes $x$ (The orbit $G \cdot x$ and stabilizer $G_{x}$ of a point in a group action, Orbit-stabiliser: $G / G_{x} \to G \cdot x$ , $g G_{x} \mapsto g \cdot x$ , is a well-defined bijection, Left group actions, transitive actions, and faithful actions, Subgroup, Conjugation $x \mapsto g x g^{- 1}$ is an automorphism, The conjugacy class ${Cl}_{G} (x)$ and centralizer $C_{G} (x)$ of an element, In a group $e^{- 1} = e$ , $(g^{- 1})^{- 1} = g$ and $(g h)^{- 1} = h^{- 1} g^{- 1}$ , the order of the last product being essential).

[F3]

The transitivity of the natural action is the statement that for all $i, j \in {0, 1, 2, 3}$ there is $σ \in S_{4}$ with $σ (i) = j$ : if $i = j$ take $σ = id$ , and if $i \neq j$ take the transposition $σ = (i j)$ , which sends $i$ to $j$ by [F1]; the action is nonregular because the nonidentity element $(0 1)$ fixes the point $2$ by [F1] (Left group actions, transitive actions, and faithful actions).

[F4]

Characterization of Frobenius complements by the coset action: for a finite group $G$ and a subgroup ${1} < H < G$ , the subgroup $H$ is a Frobenius complement exactly when the left action of $G$ on $G / H$ is transitive, nonregular, and every nonidentity element of $G$ fixes at most one coset (Frobenius permutation action characterization, Left and right cosets $g H$ and $H g$ of a subgroup, $x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$ ).

Counterexample

technique · direct

1.1

The action of $S_{4}$ on ${0, 1, 2, 3}$ is transitive and nonregular by [F3]. The stabilizer $H = G_{2}$ is a subgroup by [F2]; it contains $id$ and $(0 1)$ by [F1], and it does not contain $(2 3)$ because $(2 3)$ sends $2$ to $3$ , so ${id} < H < S_{4}$ .

F1F2F3

2.1

Take $g = (2 3)$ . Then $g \notin H$ by step 1.1, and by [F2] the conjugate $g H g^{- 1}$ is the stabilizer $G_{g \cdot 2} = G_{3}$ of the letter $3$ . The permutations lying in $H \cap G_{3}$ fix both $2$ and $3$ , so by [F1] this intersection is exactly ${id, (0 1)}$ .

F1F2step 1.1

3.1

It follows that $H$ is not a Frobenius complement of $S_{4}$ : with $g = (2 3) \notin H$ one has $H \cap g H g^{- 1} = {id, (0 1)} \neq {id}$ , whereas a Frobenius complement must satisfy $H \cap x H x^{- 1} = {1}$ for every $x \in S_{4} ∖ H$ .

F4step 2.1

4.1

The same failure is visible in the coset picture. The map $S_{4} / H \to {0, 1, 2, 3}$ , $σ H \mapsto σ (2)$ , is a bijection, and it is equivariant for the left action on cosets and the natural action on letters: $τ \cdot (σ H) = (τ σ) H \mapsto (τ σ) (2) = τ (σ (2))$ for all $τ, σ \in S_{4}$ . So the coset action is the natural action on four letters; it is transitive and nonregular by [F3], and the transposition $(0 1)$ fixes the two letters $2$ and $3$ by [F1], hence fixes the two corresponding cosets, violating the condition in [F4] that a nonidentity element fix at most one coset. Therefore the natural transitive action of $S_{4}$ on four letters is not a Frobenius action. ∎

F1F4step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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

Alex Bartel, Introduction to Representation Theory of Finite Groups, §6.1 (standard reference, not scraped)