Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-16
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.

For n≥2, Sn≅An⋊C2 using any transposition complement

Example

For every n≥2 and every transposition τ∈Sn,

Sn≅An⋊⟨τ⟩≅An⋊C2.

Facts & Assumptions

Given: An integer n≥2 and a transposition τ∈Sn.

[L1]

The sign map sgn⁡:Sn→{1,−1} is a surjective homomorphism for n≥2 (The sign is a homomorphism Sn→{+1,−1}, surjective exactly when n≥2).

[L2]

The alternating group An is the kernel of the sign homomorphism (The alternating group An=ker⁡(sgn⁡) of even permutations).

[L4]

A normal factor and a complement with trivial intersection give an external semidirect product by conjugation ( Recognition theorem: G=NH with N⊴G, N∩H=1 exactly realises an external semidirect product).

[L5]

Sn consists of the permutations of an n-element set (The symmetric group Sym⁡(X): the bijections of a set X under composition).

Verification

technique · direct
1.1L1L2L3L5

By [L1]--[L3], An is normal. The transposition τ has sign −1, so ⟨τ⟩={1,τ} intersects An trivially.

1.2L1algebra

If σ∈Sn is even, then σ∈An. If it is odd, then στ is even and σ=(στ)τ. Hence Sn=An⟨τ⟩.

2.1step 1.1step 1.2L4∎

The recognition theorem [L4] gives the asserted decomposition, with the action on An given by conjugation by τ.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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