TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Hall–Burnside: coprime automorphisms are detected on the Frattini quotient

Statement

Let $P$ be a finite $p$ -group, and let $A \leq Aut (P)$ be a finite subgroup whose order is not divisible by $p$ . If $A$ acts trivially on $P / Φ (P)$ through $ρ_{P}$ , then $A = 1$ .

Facts & Assumptions

Given: A finite $p$ -group $P$ and a finite $p^{'}$ -subgroup $A \leq Aut (P)$ acting trivially on $P / Φ (P)$ .

[L1]

A subset $X \subseteq P$ is minimally generating exactly when the quotient map restricts to a bijection from $X$ onto a basis of $P / Φ (P)$ (Burnside Basis Theorem).

[L2]

If a prime $q$ divides the order of a finite group, that group contains an element of order $q$ (Cauchy's theorem: if a prime $p$ divides $∣ G ∣$ , then $G$ has an element of order $p$ ).

[L3]

If a finite $q$ -group acts on a finite set whose size is not divisible by $q$ , then it has a fixed point (A finite $p$ -group action on $X$ has a global fixed point whenever $p ∤ ∣ X ∣$ ).

[L4]

Every automorphism of $P$ induces its action on $P / Φ (P)$ through $ρ_{P}$ (Automorphisms act linearly on the Frattini quotient).

[L5]

The order of a subgroup divides the order of a finite group (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $A \neq 1$ . Choose a prime $q$ dividing $∣ A ∣$ ; [L2] gives $α \in A$ of order $q$ . Since $p ∤ ∣ A ∣$ , one has $q \neq p$ .

givenL2assume-contraalgebra

2.1

Triviality of the quotient action in [L4] means that $α$ preserves each coset of $Φ (P)$ . Each coset has $∣ Φ (P) ∣$ , a power of $p$ by [L5], elements. The cyclic $q$ -group $⟨ α ⟩$ acts on that coset, and $q \neq p$ makes [L3] provide an $α$ -fixed representative in every coset.

step 1.1L3L4L5givenalgebra

3.1

Starting from the finite generating set $P$ , delete redundant elements until a minimal generating set remains; [L1] sends it bijectively onto a basis of $P / Φ (P)$ . Using step 2.1, choose a fixed representative of each of these finitely many basis cosets. By [L1] those representatives generate $P$ . Since $α$ fixes every generator, it fixes every element of $P$ , so $α$ is the identity, contradicting its prime order.

step 2.1L1givenalgebra

4.1

The contradiction shows that the assumed nontrivial $p^{'}$ -subgroup cannot exist; hence $A = 1$ .

step 1.1step 3.1discharge-contradiction∎

Depends on

Used by

Dependency tree · two levels

36 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

D. A. Craven, The Theory of p-Groups, Theorem 2.30 (standard reference, not scraped)