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

The socle is characteristic and decomposes as a direct product of minimal normal subgroups

Statement

Let G be a finite group. Then soc(G) is a characteristic subgroup of G. Moreover, for some integer r0 there are pairwise distinct minimal normal subgroups N1,,NrG such that

soc(G)=N1××Nr.

Here the case r=0 means the empty direct product, namely the trivial group.

Facts & Assumptions

Given: A finite group G.

[L1]

Distinct minimal normal subgroups of G centralize one another (Distinct minimal normal subgroups centralize one another).

[L2]

Every nontrivial finite characteristically simple group is a direct product of isomorphic simple groups (Finite characteristically simple groups are direct products of isomorphic simple groups).

[L3]

Every minimal normal subgroup of a finite group is characteristically simple (Minimal normal subgroups of finite groups are characteristically simple).

[A1]

Automorphisms of G permute its minimal normal subgroups.

Proof

technique · direct
1.1

By [A1], the subgroup generated by all minimal normal subgroups of G is stable under every automorphism of G. By definition this subgroup is soc(G), so soc(G) is characteristic in G.

givenA1
1.2

Let N1,,Nr be a maximal family of pairwise distinct minimal normal subgroups of G chosen so that none is contained in the product of the preceding ones; when G=1, this family is empty. For i1, [L1] shows that Ni centralizes N1Ni1, and minimality gives Ni(N1Ni1)=1 because the intersection is a normal subgroup of G contained in Ni but Ni was chosen outside the preceding product. Hence N1Nr is an internal direct product, with the case r=0 giving the trivial group.

L1choose
2.1

The product N1Nr is generated by minimal normal subgroups, so it lies in soc(G). Conversely, if M is any minimal normal subgroup of G not contained in N1Nr, then adjoining M would contradict maximality of the chosen family; therefore every minimal normal subgroup of G lies in the displayed product. Thus soc(G)=N1××Nr. By [L3], each nontrivial factor Ni is characteristically simple, and [L2] then makes it a direct product of isomorphic simple groups.

step 1.2L2L3

Depends on

Used by

Dependency tree · two levels

14 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