ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

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.

With trivial C_2-action on S_3, the nonabelian H^1 pointed set has two classes

Example

For the trivial action of $C_{2}$ on $S_{3}$ , the pointed set $H_{n a b}^{1} (C_{2}, S_{3})$ has exactly two elements.

Facts & Assumptions

Given: The trivial action of $C_{2}$ on $S_{3}$ (The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition).

[L1]

Nonabelian first cohomology is the orbit set of crossed homomorphisms under coefficient-group conjugation (First nonabelian cohomology as a pointed set).

[L2]

It classifies complements as a pointed set (Nonabelian first cohomology classifies complements as a pointed set).

Verification

technique · direct

1.1

Under the trivial action, a cocycle is just a homomorphism $C_{2} \to S_{3}$ . The image of the generator is therefore either the identity or an element of order $2$ , that is, a transposition.

givenL1algebra

2.1

All transpositions are conjugate in $S_{3}$ , so [L1] leaves exactly two orbits of cocycles: the trivial one and the orbit of any transposition-valued cocycle. Thus $H_{n a b}^{1} (C_{2}, S_{3})$ has two points, with the trivial one as basepoint. This matches the complement picture from [L2].

L1L2step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

Chaoli Li, Class field theory: proofs (standard reference, not scraped)