CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Generation of a finite group is detected modulo its Frattini subgroup

Statement

A subset $S$ of a finite group $G$ generates $G$ if and only if its image generates $G / Φ (G)$ (The Frattini subgroup $Φ (G)$ as the intersection of the maximal subgroups of a finite group).

Facts & Assumptions

Given: A finite group $G$ , its normal subgroup $Φ (G)$ from The Frattini subgroup of a finite group is characteristic, the quotient map $π : G \to G / Φ (G)$ , and a subset $S \subseteq G$ .

[L1]

For a finite group $G$ , an element $x$ lies in $Φ (G)$ if and only if, for every subset $T \subseteq G$ , $⟨ T, x ⟩ = G$ implies $⟨ T ⟩ = G$ (The Frattini subgroup consists exactly of the nongenerators of a finite group).

[L2]

For $N ⊴ G$ , subgroups of $G / N$ correspond inclusion-preservingly to subgroups of $G$ containing $N$ (Correspondence theorem: subgroups of $G / N$ correspond to subgroups of $G$ containing $N$ , with normality preserved).

Proof

technique · direct

1.1givenL2

If $⟨ S ⟩ = G$ , then applying the quotient map gives $⟨ π (S) ⟩ = G / Φ (G)$ .

1.2givenL1algebra

Conversely, suppose $π (S)$ generates the quotient. Then $⟨ S, Φ (G) ⟩ = G$ . The subgroup $Φ (G)$ is finite, so list its elements and remove them one at a time from this generating set: [L1] says each is a nongenerator. After all have been removed, $⟨ S ⟩ = G$ .

2.1step 1.1step 1.2L2∎

Steps 1.1 and 1.2 prove both implications. When $G = 1$ , both the empty subset and its empty quotient image generate, so the boundary case also agrees.

Depends on

Used by

Dependency tree · two levels

13 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, Proposition 2.18 (standard reference, not scraped)
K. Conrad, Generating Sets, Theorem 6.12 (standard reference, not scraped)