ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11

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.

There are six two-colourings of the vertices of a square up to its eight symmetries

Example

The eight symmetries of a square act on its two-colour vertex colourings. There are exactly six orbits, so there are six colourings up to symmetry.

Facts & Assumptions

Given: The square-symmetry group $D$ acting on the vertex set $V = {1, 2, 3, 4}$ and the colouring set $C = {0, 1}^{V}$ .

[L1]

Orbit counting gives $∣ D ∣ ∣ C / D ∣ = \sum_{g \in D} ∣ C^{g} ∣$ (Cauchy-Frobenius orbit counting: $∣ G ∣ ∣ X / G ∣ = \sum_{g \in G} ∣ X^{g} ∣$ for a finite group action).

[L2]

The group $D$ has eight elements: four rotations and four reflections (The square-symmetry group has class equation $8 = 2 + 2 + 2 + 2$ ).

[L3]

A left action satisfies the usual identity and product laws (Left group actions, transitive actions, and faithful actions).

[L4]

There are $2^{4} = 16$ functions $V \to {0, 1}$ (The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$ ).

Verification

technique · direct

1.1

Define $(g \cdot c) (v) = c (g^{- 1} v)$ . Inverse precomposition gives $e \cdot c = c$ and $(g h) \cdot c = g \cdot (h \cdot c)$ , so [L2] and [L3] give an action on the $16$ colourings counted by [L4].

L2L3L4

2.1

A colouring fixed by a symmetry is constant on each cycle of that symmetry. Thus the identity fixes $16$ colourings; the two quarter-turns fix $2$ each; the half-turn fixes $4$ ; the two reflections through opposite vertices fix $8$ each; and the two reflections through opposite edges fix $4$ each.

step 1.1L2algebra

3.1

The fixed-point sum is $16 + 2 + 2 + 4 + 8 + 8 + 4 + 4 = 48$ . By [L1] and $∣ D ∣ = 8$ , one has $48 = 8 ∣ C / D ∣$ , so $∣ C / D ∣ = 6$ .

step 2.1L1L2algebra

4.1

The six orbits can also be distinguished by the number of black vertices, with the two-black case split into adjacent and opposite pairs, confirming the count.

step 3.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

T. W. Judson, Abstract Algebra: Theory and Applications, 14.3 (standard reference, not scraped)