ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 dihedral group of order eight has Cayley graphs that are a cycle of length eight and a cube

Example

The dihedral group of order eight has Cayley graphs that are a cycle of length eight and a cube.

Facts & Assumptions

Given: The objects and hypotheses in the Example.

[F1]

The Cayley graph of a group $G$ with respect to a subset $S$ has vertex set $G$ and edge set ${{g, g s} : g \in G, s \in (S \cup S^{- 1}) ∖ {e}}$ (The Cayley graph of a group with respect to a subset).

[L1]

Every vertex of a Cayley graph has the same degree, and the graph is locally finite exactly when the symmetrised generating set is finite (Cayley-graph neighbourhoods are equipotent, and local finiteness is equivalent to finiteness of the symmetrised subset).

[L2]

For $D = Dih (C_{4}) = ⟨ r, s ⟩$ , one has $r^{4} = s^{2} = 1$ , $s r s^{- 1} = r^{- 1}$ , and every element is uniquely $r^{i}$ or $r^{i} s$ for $0 \leq i < 4$ ( $Dih (C_{n}) = C_{n} ⋊ C_{2}$ with inversion action has order $2 n$ and the dihedral relations).

[L3]

$Dih (A) = A ⋊ C_{2} .$ ( The generalized dihedral group $Dih (A) = A ⋊ C_{2}$ for an abelian group $A$ ).

[L4]

The degree of $v$ is $\deg_{G} (v) : = ∣ N_{G} (v) ∣$ , equivalently the number of edges incident with $v$ . A graph is $r$ -regular when every vertex has degree $r$ ; it is cubic when it is $3$ -regular. (Adjacency, incidence, open and closed neighbourhoods, vertex degree, minimum degree and maximum degree).

Verification

technique · direct

1.1

For the generating set ${r, s}$ , the four vertices $1, r, r^{2}, r^{3}$ form a $4$ -cycle under right multiplication by $r^{\pm 1}$ , and the four vertices $s, r s, r^{2} s, r^{3} s$ form another. Right multiplication by $s$ joins $r^{i}$ to $r^{i} s$ for each $i$ . Thus the graph is two $4$ -cycles joined at corresponding vertices, which is the cube.

F1L1L2L3L4

2.1

For the generating set ${s, r s}$ both generators are involutions and they generate because $(r s) s = r$ . Alternating them gives the eight-cycle $1, s, r^{3}, r^{3} s, r^{2}, r^{2} s, r, r s, 1$ , whose consecutive vertices differ by right multiplication by $s$ or $r s$ . These are all eight group elements, and every vertex has only the two displayed neighbours, so this Cayley graph is $C_{8}$ .

F1L1L2L4step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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

D. A. Craven, The Theory of p-Groups (Hilary Term 2008), 48 pp. (standard reference, not scraped)
M. van Beek, Topics in Finite p-Groups, 62 pp. (standard reference, not scraped)
D. Kaur and A. Kulshrestha, Characters of real special 2-groups (arXiv:1510.06583v1) (standard reference, not scraped)