Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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.

In a finite group, every element g satisfies gn=e for some natural n≥1

Statement

Let G be a group (Group and abelian group) whose underlying set is finite (Finite, countably infinite, countable, uncountable), and let g∈G. Then there is a natural number n≥1 with gn=e, the power being the natural power of Powers gn: natural exponents in a monoid and integer exponents in a group, with g0=e.

Facts & Assumptions

Given: A group G with identity e whose underlying set is finite, and an element g∈G; natural powers gk with g0=e and gσ(k)=gkg (Powers gn: natural exponents in a monoid and integer exponents in a group, with g0=e).

[L1]

G finite means G≈m for some m∈N, that is, there is a bijection β:G→m (Finite, countably infinite, countable, uncountable, Equinumerous sets, A≈B and A⪯B).

[L2]

Claim 1 of the pigeonhole principle: for every m∈N there is no injection σ(m)→m (The pigeonhole principle on N).

[L3]

On N the order is membership, so the elements of the natural number σ(m) are exactly the natural numbers k<σ(m), and the elements of m are exactly the natural numbers k<m (On N the order is membership: m<n  ⟺  m∈n, The natural numbers N (von Neumann)).

[L4]

A map f is injective when f(x)=f(y) forces x=y; a bijection is injective (Injection, surjection, bijection).

[L7]

On N: exactly one of i<j, i=j, j<i holds (Trichotomy of the order on N); i≤j means i+k=j for some k (Order on the natural numbers); every k≠0 is a successor σ(t)=1+t (Every nonzero natural number is a successor, Addition is commutative), so k≠0 implies 1≤k.

Proof

technique · direct
1.1

Fix a bijection β:G→m with m∈N, available because G is finite.

L1choose
2.1

Define F:σ(m)→m by F(k):=β(gk). This is a function: every element k of σ(m) is a natural number, so the natural power gk is defined and lies in G, and β sends it into m.

step 1.1L3given
3.1

F is not injective, since there is no injection σ(m)→m. Hence there are i,j∈σ(m) with i≠j and F(i)=F(j).

step 2.1L2choose
4.1

From β(gi)=β(gj) and injectivity of β we get gi=gj.

step 1.1step 3.1L4
4.2

By trichotomy and i≠j, one of i<j and j<i holds; interchanging the names if necessary, assume i<j. Then i+k=j for some k∈N, and k≠0, since k=0 would give i=j.

step 3.1L7
5.1

Hence gigk=gi+k=gj=gi=gie, and cancelling gi on the left gives gk=e.

step 4.1step 4.2L5L6given
6.1

Finally k≠0 gives 1≤k, so n:=k is a natural number with n≥1 and gn=e.

step 4.2step 5.1L7∎

Remarks

  • The route avoids "a subset of a finite set is finite". That statement is not available at this point in the reading order, so the argument does not build an injection N→G and contradict finiteness. It uses claim 1 of The pigeonhole principle on N directly on the map k↦β(gk) from σ(m) to m: the m+1 exponents 0,1,…,m cannot receive m+1 distinct values in a set of m elements.

  • The conclusion is one-sided on purpose. It asserts that some positive power is the identity, not which one. Picking the least such power is what defines ord⁡(g) (The order ∣G∣ of a finite group and the order ord⁡(g) of an element, with ord⁡(g)=∞ when no positive power of g is the identity), and that step needs the well-ordering principle, not this lemma.

  • The hypothesis of finiteness cannot be dropped: in (Z,+) the element 1 satisfies n⋅1=n≠0 for every n≥1.

Depends on

Used by

Dependency tree · two levels

45 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