Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedSession-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.

The four rotations of a square act freely, transitively and faithfully on its vertices

Example

Label the vertices of a square by Z/4\mathbb Z/4 in cyclic order. The rotation group Z/4\mathbb Z/4 acts by a⋅x=a+xa\cdot x=a+x. This action is free, transitive, and faithful.

Facts & Assumptions

Given: The additive group A=Z/4A=\mathbb Z/4 acting on X=AX=A by translation.

[L1]

A left action is transitive and faithful as defined in Left group actions, transitive actions, and faithful actions.

[L2]

An action is free when only the identity can fix a point (A free group action has no nonidentity element fixing a point).

[L3]

The residue classes modulo 44 form an additive group (For every natural nn, (Z/n,+)(\mathbb{Z}/n,+) is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

[L4]

The four classes have unique representatives 0,1,2,30,1,2,3 (For n≥1n\ge 1, every class in Z/n\mathbb{Z}/n has one representative rr with 0≤r<n0\le r<n, so ∣Z/n∣=n\lvert\mathbb{Z}/n\rvert=n; while Z/0\mathbb{Z}/0 is in bijection with Z\mathbb{Z}).

Verification

technique · direct
1.1

One has 0⋅x=x0\cdot x=x and (a+b)⋅x=(a+b)+x=a+(b+x)=a⋅(b⋅x)(a+b)\cdot x=(a+b)+x=a+(b+x)=a\cdot(b\cdot x), so [L1] and [L3] give an action.

L1L3
2.1

Given vertices x,yx,y, the unique class a=y−xa=y-x satisfies a⋅x=ya\cdot x=y, proving transitivity. If a⋅x=xa\cdot x=x, cancellation gives a=0a=0, so the action is free.

step 1.1L1L2L3L4
3.1

An element fixing every vertex fixes 00, so it is 00 by step 2.1; hence the action is faithful.

step 2.1L1∎

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: 52 results over 11 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