Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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 Sylow subgroups of S4

Example

The group S4 has three Sylow 2-subgroups, each of order 8, and four Sylow 3-subgroups, each generated by a pair of inverse 3-cycles. See The number np(G) of Sylow p-subgroups.

Facts & Assumptions

Given: The hypotheses and objects in the Example.

[L1]

For a finite group G and a prime p, let Sylp(G) be the set of Sylow p-subgroups (def-sylow-p-subgroup). Define np(G):=Sylp(G). This cardinal is defined even before existence is proved because Sylp(G) is a subset of the finite power set of G; thm-sylow-first-theorem later shows it is nonzero. (The number np(G) of Sylow p-subgroups).

[L2]

Let G=pam with pm. Then the number of Sylow p-subgroups satisfies np(G)1(modp),np(G)m.. (Sylow III: np1(modp) and npm when G=pam with pm).

[L3]

Let nN, so that n={0,1,,n1} (def-natural-numbers). The symmetric group on n letters is Sn:=Sym(n)=Sym({0,1,,n1}), the group of all bijections of n under composition (def-symmetric-group), with the composition convention. (The finite symmetric group Sn, one-line notation, and cycle notation).

[L4]

For σ,τSn, there is a gSn with τ=gσg1 if and only if σ and τ have the same cycle type, including their numbers of fixed points. (Two elements of Sn are conjugate if and only if they have the same cycle type).

Verification

technique · direct
1.1

Relabel the underlying set as {1,2,3,4}. Each of its three partitions into two unordered pairs has a stabilizer of order 222=8: one may swap within either pair and may swap the two pairs. These three distinct stabilizers are therefore Sylow 2-subgroups.

L1L2L3L4givenalgebra
2.1

A subgroup of order 3 is generated by a 3-cycle. Choosing its unique fixed point gives four subgroups, because the two cycles on the remaining three letters are inverse generators of the same subgroup. Thus n2=3 and n3=4, consistent with n23, n21(mod2), n38, and n31(mod3). This proves the stated claim.

step 1.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: 43 results over 12 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