TheoremStatement: Literature-sourcedProof: 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.

Cauchy-Frobenius orbit counting: $|G|\,|X/G|=\sum_{g\in G}|X^g|$ for a finite group action

Statement

Let a finite group $G$ act on a finite set $X$ , and let $X/G$ denote the set of orbits. Then

$|G|\,|X/G|=\sum_{g\in G}|X^g|.$

Equivalently, the number of orbits is the average number of fixed points of an element of $G$ .

Facts & Assumptions

Given: A finite group $G$ acting on a finite set $X$ .

[L1]

The fixed-point set of $g$ is $X^g=\{x\in X:g\cdot x=x\}$ (The fixed-point sets $X^g$ and $X^G$ of a group action).

[L2]

The orbits partition $X$ (The orbits of a group action are the equivalence classes of $x\sim y$ iff $y=g\cdot x$ for some $g$ , and hence partition the acted-on set).

[L3]

For every $x\in X$ , $|G|=|G_x|\,|G\cdot x|$ (Orbit-stabiliser cardinality: $|G\cdot x|=[G:G_x]$ whenever either side is finite, and $|G|=|G_x|\,|G\cdot x|$ for finite $G$ ).

[L4]

A finite incidence relation can be counted by either family of fibres (Double counting: $\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^y\rvert$ for a relation between finite sets).

[L5]

Finite sums over finite index sets are well-defined (The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form).

[L6]

A finite sum splits along a finite partition of its index set (The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition).

Proof

technique · direct

1.1

Let $R=\{(g,x)\in G\times X:g\cdot x=x\}$ . Counting its fibres over $g$ and using [L1], [L4], and [L5] gives $|R|=\sum_{g\in G}|X^g|$ .

L1L4L5

1.2

Counting the same relation over $x$ gives $|R|=\sum_{x\in X}|G_x|$ .

L4L5

2.1

Split the second sum along the orbit partition using [L2] and [L6]. On an orbit $O=G\cdot x$ , [L3] gives $|G_y|=|G|/|O|$ for every $y\in O$ , so that orbit contributes $|O|(|G|/|O|)=|G|$ .

step 1.2L2L3L5L6

3.1

There is one contribution for each orbit in $X/G$ , hence $|R|=|G|\,|X/G|$ . Combining this with step 1.1 gives the stated identity.

step 1.1step 2.1L2L5∎

Depends on

Used by

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, Burnside's Counting Theorem (standard reference, not scraped)
K. Conrad, Group Actions, Theorem 3.29 (standard reference, not scraped)

Cauchy-Frobenius orbit counting: ∣G∣ ∣X/G∣=∑g∈G∣Xg∣|G|\,|X/G|=\sum_{g\in G}|X^g|∣G∣∣X/G∣=∑g∈G​∣Xg∣ for a finite group action