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 Finite Simple Group Classification Landscape — Examples
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Conjugacy in Sₙ, Generation, and the Simplicity of Aₙ
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Cyclic Groups and Direct Products
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Normal Subgroups and Quotient Groups
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Relations, Functions, and Quotients
- Roots, Rational Powers, and Classical Inequalities
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The ZFC Axioms and the Basic Set Constructions
2 · Summary
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Cyclic simple groups of prime order
Example
is finite simple for every prime .
Facts & Assumptions
Given: Let be prime.
Verification
The group has order , so Lagrange's theorem leaves only subgroups of orders and . Thus it has no nontrivial proper normal subgroup.
Hence is finite and simple.
A5 as the smallest nonabelian simple group
Example
is the smallest nonabelian finite simple group.
Facts & Assumptions
Given: The alternating group and finite groups of order less than .
is simple for ( is simple for every ).
If with , then and (Sylow III: and when with ). The Sylow subgroups form a single conjugacy class (Sylow II: in a finite group every -subgroup lies in a conjugate of any Sylow -subgroup, and the Sylow -subgroups form a single conjugacy class), and a unique Sylow subgroup is normal (A Sylow -subgroup is normal if and only if it is unique).
A nontrivial finite -group has nontrivial center (Every nontrivial finite -group has nontrivial center, in fact divides ).
Subgroup orders divide group orders (Lagrange's theorem: for every subgroup of a finite group ); is the kernel of sign (The alternating group of even permutations).
Verification
By [L1], is simple. Multiplication by a transposition pairs the even and odd permutations, so . The even permutations and do not commute: whereas . Thus is nonabelian.
Suppose is nonabelian simple and . Its order cannot be or a prime power: in the latter case its nontrivial normal center from [L3] would be all of , making abelian. For every prime divisor of its order, [L2] therefore gives .
The non-prime-power integers between and , apart from , are For each integer in this list, take its largest prime divisor . Inspection of the divisors of shows that is the only divisor congruent to modulo . Thus [L2] gives , excluding every order in the list.
A nontrivial conjugation action of a simple group on its Sylow subgroups is faithful: the kernel is normal and cannot be all of , because the action is transitive. Thus embeds in . The sign of this action is trivial, since a nontrivial homomorphism from nonabelian simple to the group of order two would be injective. Consequently embeds in . For orders , [L2] gives . Since , [L4] rules out ; at order the image would be all of , which is not simple: its identity and three double transpositions form a proper nontrivial subgroup preserved by conjugation. For order , [L2] gives , contradicting an embedding of into , of order .
For order , [L2] and step 1.2 force and . Distinct subgroups of prime order intersect only in the identity by [L4], so these supply distinct nonidentity elements, impossible. For order , the same rules give and . The eight subgroups of order supply distinct nonidentity elements. Every Sylow -subgroup has order , and its seven nonidentity elements must be the seven remaining nonidentity elements of . All Sylow -subgroups would therefore coincide, contradicting .
Steps 1.2–2.2 exclude every order below , while step 1.1 supplies a nonabelian simple group of order . Hence is the smallest nonabelian finite simple group. [step 1.1, step 1.2, step 2.1, step 2.2, step 2.3].
PSL(2,7) and a low-rank family entry
Example
is a sourced Lie-type entry under the table's low-rank convention.
Facts & Assumptions
Given: Use Smith's Lie-type family table and its rank-one notation cited above.
Smith's table lists type as the linear family , and its rank-one discussion explicitly names as Lie type. In standard notation .
Verification
Specializing [L1] to and places in the linear Lie-type family.
This is precisely the claimed table-level Lie-type example; no structural construction is being inferred.
A Suzuki group family entry
Example
Suzuki groups occur in the source’s nonclassical twisted row.
Facts & Assumptions
Given: Use Smith's nonclassical twisted-family row cited above.
Smith's nonclassical twisted-family row includes the Suzuki groups among the finite simple groups of Lie type.
Verification
That row explicitly includes the Suzuki family among the finite simple groups of Lie type.
Hence Suzuki groups furnish the asserted named-family entry.
Composition factors do not determine the extension
Statement refuted
C4 and C2×C2 share composition factors but are not isomorphic.
Counterexample
Given: Use the two groups in the statement.
Their simple factors agree while their element orders differ.
Thus they provide the asserted counterexample.