Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17
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.

The Frattini subgroup consists exactly of the nongenerators of a finite group

Statement

For a finite group G, an element x lies in Φ(G) if and only if, for every subset S⊆G, ⟨S,x⟩=G implies ⟨S⟩=G. See The Frattini subgroup Φ(G) as the intersection of the maximal subgroups of a finite group.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

For a finite group G, the Frattini subgroup is Φ(G):=⋂{M≤G:M is maximal proper}. If G=1, the family is empty and its intersection inside G is G itself. Thus Φ(1)=1. (The Frattini subgroup Φ(G) as the intersection of the maximal subgroups of a finite group).

[L2]

For a subset S of a group G, the generated subgroup is ⟨S⟩:=⋂{H:H≤G and S⊆H}, the smallest subgroup of G containing S. (The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups).

Proof

technique · direct
1.1

If x∉Φ(G), a maximal subgroup omitting x shows that adjoining x can enlarge a generating set.

L1L2givenalgebra
2.1

Conversely, if ⟨S,x⟩=G while ⟨S⟩≠G, extend the latter finite subgroup to a maximal subgroup; it contains S but cannot contain x.

step 1.1givenalgebra
3.1

We treat the trivial group, whose empty intersection convention gives Φ(1)=1. This proves the stated claim.

step 2.1givenalgebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 12 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources