TheoremStatement: AI-adaptedProof: 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.

Any two finite free bases of the same group have the same cardinality

Statement

If $B$ and $C$ are finite free bases of the same group $F$ , then $|B|=|C|$ .

Facts & Assumptions

Given: A group $F$ with finite free bases $B$ and $C$ , and the group $C_2:=\operatorname{Sym}(\{0,1\})$ .

[L1]

If $A$ and $B$ are finite, then $A^B$ is finite and $|A^B|=|A|^{|B|}$ (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}$ ).

[L2]

For $m,n\in\mathbb N$ , the natural number $m^n$ and the real number $m^n$ agree under the canonical inclusion $\mathbb N\subseteq\mathbb R$ (Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ ).

[L3]

If $a>1$ , then $a^m<a^n$ whenever $m<n$ in $\mathbb N$ (Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$ ).

[L4]

For naturals $m,n$ , exactly one of $m<n$ , $m=n$ , $m>n$ holds (Trichotomy of the order on $\mathbb{N}$ ).

[L5]

$(\operatorname{Sym}(X),\circ,\operatorname{id}_X)$ is a group for every set $X$ ( $\operatorname{Sym}(X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements).

[F1]

If $A$ is finite and $f:A\to B$ is a bijection, then $B$ is finite and $|B|=|A|$ (The cardinality $\lvert A\rvert$ of a finite set).

Proof

technique · direct

1.1

Every permutation of $\{0,1\}$ is determined by the image of $0$ : it is either the identity or the transposition $(0\,1)$ , and these two maps are distinct; hence $C_2$ is a group with exactly two elements.

L5algebra

2.1

Restriction to $B$ maps $\operatorname{Hom}(F,C_2)$ to the function set $C_2^B$ , and the free-basis property gives a unique homomorphic extension of every function $B\to C_2$ ; restriction and extension are inverse maps, so restriction is a bijection $\operatorname{Hom}(F,C_2)\to C_2^B$ ; [L1] counts $|C_2^B|=2^{|B|}$ and [F1] transports that count along the bijection, giving $|\operatorname{Hom}(F,C_2)|=2^{|B|}$ , including $B=\varnothing$ .

F1L1step 1.1given

3.1

Applying the same restriction-extension bijection to $C$ gives $|\operatorname{Hom}(F,C_2)|=2^{|C|}$ , and therefore $2^{|B|}=2^{|C|}$ as natural numbers.

step 2.1given

4.1

If $|B|<|C|$ , then [L2] lets the equality of step 3.1 be read in $\mathbb R$ , and [L3] applied to the base $2>1$ gives $2^{|B|}<2^{|C|}$ , contradicting step 3.1; the case $|C|<|B|$ is symmetric, so trichotomy [L4] forces $|B|=|C|$ .

L2L3L4step 3.1algebra

5.1

Thus any two finite free bases of $F$ , including empty bases, have the same cardinality.

step 4.1∎

Depends on

Used by

The rank of a free group admitting a finite basis Definition

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 83 results over 22 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

Richard Elman, Lectures on Abstract Algebra, §18 (standard reference, not scraped)
Encyclopedia of Mathematics, Free group (standard reference, not scraped)