Alphabeta MathHow 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 binary necklaces of length four up to rotation
Example
Binary words of length four, considered up to cyclic rotation, form six orbits. Equivalently, there are six binary necklaces of length four.
Facts & Assumptions
Given: The additive group acting by rotation on the binary words .
Orbit counting gives (Cauchy-Frobenius orbit counting: for a finite group action).
A left action satisfies the identity and product laws (Left group actions, transitive actions, and faithful actions).
The residue classes modulo form an additive group (For every natural , is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).
The four classes are represented by (For , every class in has one representative with , so ; while is in bijection with ).
The set of binary functions on a four-element set has elements (The set of functions between finite sets is finite, with ).
Verification
Let . Addition in [L3] verifies the action laws [L2], and [L4] and [L5] give four rotations acting on words.
Rotation by fixes all words; rotations by and each force all positions equal and fix words; rotation by permits one colour on each opposite pair and fixes words.
The fixed-point sum is , so [L1] gives and hence .
Depends on
- Cauchy-Frobenius orbit counting: $|G|\,|X/G|=\sum_{g\in G}|X^g|$ for a finite group action
- Left group actions, transitive actions, and faithful actions
- For every natural $n$, $(\mathbb{Z}/n,+)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold
- For $n\ge 1$, every class in $\mathbb{Z}/n$ has one representative $r$ with $0\le r<n$, so $\lvert\mathbb{Z}/n\rvert=n$; while $\mathbb{Z}/0$ is in bijection with $\mathbb{Z}$
- 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}$
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: 84 results over 20 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)