Alphabeta Math
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.

Left multiplication gives a free and transitive action of every group on itself

Example

Every group GG acts on its underlying set by left multiplication, g⋅x=gxg\cdot x=gx. This left regular action is free and transitive, and every stabilizer is the trivial subgroup.

Facts & Assumptions

Given: A group GG acting on its underlying set by g⋅x=gxg\cdot x=gx.

[L1]

A left action satisfies e⋅x=xe\cdot x=x and (gh)⋅x=g⋅(h⋅x)(gh)\cdot x=g\cdot(h\cdot x) and is transitive when some group element carries any point to any other (Left group actions, transitive actions, and faithful actions).

[L2]

An action is free when g⋅x=xg\cdot x=x implies g=eg=e (A free group action has no nonidentity element fixing a point).

[L3]

The stabilizer is Gx={g:g⋅x=x}G_x=\{g:g\cdot x=x\} (The orbit G⋅xG\cdot x and stabilizer GxG_x of a point in a group action).

Verification

technique · direct
1.1

The identities e⋅x=ex=xe\cdot x=ex=x and (gh)⋅x=(gh)x=g(hx)=g⋅(h⋅x)(gh)\cdot x=(gh)x=g(hx)=g\cdot(h\cdot x) verify the action laws.

L1algebra
2.1

Given x,y∈Gx,y\in G, the element g=yx−1g=yx^{-1} satisfies g⋅x=yg\cdot x=y, so the action is transitive.

step 1.1L1choosealgebra
3.1

If g⋅x=xg\cdot x=x, then gx=xgx=x and right cancellation gives g=eg=e; by [L2] the action is free, and [L3] gives Gx={e}G_x=\{e\} for every xx.

step 1.1L2L3algebra∎

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: 9 results over 8 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