Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13
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 Jordan–Hölder theorem for groups

Statement

If a group G has two composition series, then the series have the same length and their composition factors agree up to isomorphism and permutation.

Facts & Assumptions

Given: Two composition series of the same group G.

[F1]

A composition series is a strictly descending subnormal series with simple factors (Composition series, composition factors, and composition length).

[L1]

Any two finite subnormal series of a group have equivalent refinements (The Schreier refinement theorem).

[L2]

For N⊴H, the maps K↦K/N and inverse image under H→H/N give inverse inclusion-preserving bijections between subgroups above N and subgroups of H/N, and they preserve normality (Correspondence theorem: subgroups of G/N correspond to subgroups of G containing N, with normality preserved).

Proof

technique · direct
1.1

By [L1], the two composition series have equivalent refinements.

givenL1
1.2

A subnormal refinement cannot insert a term strictly between adjacent terms H▹N: the first inserted term K would satisfy N<K<H and K⊴H, so [L2] would make K/N a nontrivial proper normal subgroup of the simple factor H/N.

F1L2
2.1

Therefore each refinement differs from its original composition series only by repeated adjacent terms, and deleting those repetitions recovers the original series.

step 1.2
3.1

Equivalence of the refinements now pairs the original nontrivial factors; hence the two series have the same number of factors, and a permutation matches their factors up to isomorphism.

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 27 results over 11 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