ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$ ).

Verification

technique · direct

1.1

Define $(g\cdot c)(v)=c(g^{-1}v)$ . Inverse precomposition gives $e\cdot c=c$ and $(gh)\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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 87 results over 21 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

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