# Finite abelian group: from a complete Cayley table, group qualification first, then commutativity

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-finite-abelian-group/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-finite-abelian-group-01 · production-20261019-adopted-96



## Goal and scope

On the carrier G={0,1,2,3} a complete 4×4 Cayley table is given (the cell in row a, column b is a*b): row 0 is (1,2,3,0), row 1 is (2,3,0,1), row 2 is (3,0,1,2), row 3 is (0,1,2,3). Check closure, associativity, a unique identity and inverses in that order, then check a*b=b*a for all a, b, to decide whether (G,*) is a finite abelian group; find the orders of the elements 0 and 1 and the cyclic subgroups they generate; and use the symmetric table a∘b=|a−b| on {0,1,2} to show that a symmetric table cannot replace group qualification.

Stays inside the MKO's slice: carrier labels 0 to n−1 (here n=4) and a complete n×n table, classifying only an explicitly supplied finite table. Modular arithmetic modulo 4 gives the universal proofs, and exhaustive checks over the whole carrier serve as cross-checks. The structure theorem for finite abelian groups and other groups are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- group_axioms
- add_comm
- add_assoc
- forall_intro
- quantifier_negation
- abs_rules


- G1 — The carrier G={0,1,2,3}, with labels 0 to n−1 and n=4.
- G2 — The complete Cayley table (the cell in row a, column b is a*b): row 0 (1,2,3,0); row 1 (2,3,0,1); row 2 (3,0,1,2); row 3 (0,1,2,3).
- G3 — Contrast table: carrier K={0,1,2}, a∘b=|a−b|, that is row 0 (0,1,2), row 1 (1,0,1), row 2 (2,1,0).


- G=\{0,1,2,3\} — the carrier (labels)
- a*b — the entry in row a, column b of the table
- x\bmod 4 — the remainder of x on division by 4, a value from 0 to 3
- e — the identity element (here e=3)
- a^k,\ \operatorname{ord}(a) — the k-th power of a and the order of a
- \langle a\rangle — the cyclic subgroup generated by a





## Rules and sources


- group_axioms · prerequisite — Group axioms: a set G with a binary operation that is associative, has an identity e (eg=ge=g), and in which every g has an inverse g⁻¹ (gg⁻¹=g⁻¹g=e).
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_fag · cited — A finite abelian group must first qualify as a group using its complete Cayley table: closure, associativity, a unique identity and inverses. Then check a*b=b*a for all a, b. This slice classifies only explicitly supplied finite tables; a few commuting samples or apparently commuting generators are not used to infer commutativity of the whole group. · mko-finite-abelian-group
- table_read · prerequisite — Reading the table: a*b is the cell in row a, column b of the supplied Cayley table; a complete table has exactly one cell for every pair (a,b).
- mod_arith · prerequisite — Arithmetic modulo n (n≥1): x mod n is the unique integer r with 0≤r≤n−1 and n∣(x−r). x≡y (mod n) means n∣(x−y); it is an equivalence relation compatible with addition; x mod n≡x; two integers between 0 and n−1 that are congruent modulo n are equal.
- power_def · prerequisite — Powers and order in a group: a¹=a and a^(k+1)=a^k*a; the order of a is the least positive integer k with a^k=e; ⟨a⟩ is the set of all powers of a.
- L_id_unique · lemma — If e and e′ are both two-sided identities for the operation *, then e=e′.





## Main derivation

S01 · definitionBefore

(G,*)\ \text{finite abelian group}

After

\text{closure}\land\text{assoc}\land\text{unique } e\land\text{inverses},\ \text{then}\ \forall a,b:\ a*b=b*a

Conditions: none

Rule: mko_fag · Uses: mko_fag, group_axioms

Leaf basis: mko_fag + def_unfold

By the MKO, classification has two stages: first use the complete table to check group qualification (closure, associativity, a unique identity, inverses), and only after all of these pass check commutativity a*b=b*a for all a, b. The order cannot be reversed: commutativity makes an 'abelian group' only of a structure that is already a group.



S02 · equivalentBefore

a*b\ \text{read from the table}

After

a*b=(a+b+1)\bmod 4\ \text{for all 16 pairs}

Conditions: none

Rule: table_read · Uses: G1, G2, table_read, mod_arith

Leaf basis: table_read + mod_arith + numeric_evaluation

Compare cell by cell: row a lists, for b=0,1,2,3, the remainders of a+1, a+2, a+3, a+4 on division by 4. For example row 0 gives 1, 2, 3 and 4 mod 4=0, that is (1,2,3,0); row 2 gives the remainders of 3, 4, 5, 6, that is (3,0,1,2). All 16 cells of the four rows agree with (a+b+1) mod 4. This is an exhaustive comparison over the complete table, not a sample; afterwards modular arithmetic can argue for all elements at once.



S03 · impliesBefore

a,b\in G

After

a*b=(a+b+1)\bmod 4\in\{0,1,2,3\}=G

Conditions: none

Rule: mod_arith · Uses: S02, mod_arith

Leaf basis: mod_arith + forall_intro

Closure: a remainder on division by 4 always lies between 0 and 3, so every a*b lies in G. Reading the table gives the same: all 16 cells are among 0, 1, 2, 3.



S04 · impliesBefore

(a*b)*c,\ a*(b*c)

After

(a*b)*c=a*(b*c)\ \text{for all } a,b,c\in G

Conditions: none

Rule: mod_arith · Uses: S02, S03, mod_arith

Leaf basis: mod_arith + add_assoc + add_comm + forall_intro

Associativity must hold for all 64 triples (a,b,c). Instead of listing them, modular arithmetic proves it at once: both sides are congruent to a+b+c+2 modulo 4 (S04.1, S04.2), and both lie between 0 and 3, so they are equal (S04.3). N3 additionally cross-checks all 64 triples exhaustively.



S05 · impliesBefore

3*b,\ a*3

After

3*b=(b+4)\bmod 4=b,\ a*3=(a+4)\bmod 4=a

Conditions: none

Rule: mod_arith · Uses: S02, mod_arith

Leaf basis: mod_arith + forall_intro

Take e=3: 3*b=(3+b+1) mod 4=(b+4) mod 4=b, since b lies between 0 and 3 and b+4≡b; likewise a*3=a. Row 3 of the table, (0,1,2,3), and column 3 both reproduce the labels, consistently. Note that the identity is 3, not the label 0: 0*0=1≠0.



S06 · impliesBefore

e=3\ \text{is an identity}

After

e=3\ \text{is the unique identity}

Conditions: none

Rule: L_id_unique · Uses: S05, L_id_unique

Leaf basis: L_id_unique

The MKO requires the identity to be unique. By Lemma L_id_unique (proved in S06.1), any other two-sided identity e′ equals 3.



S07 · impliesBefore

a\in G

After

a^{-1}=(2-a)\bmod 4:\ 0\leftrightarrow 2,\ 1\leftrightarrow 1,\ 3\leftrightarrow 3

Conditions: none

Rule: mod_arith · Uses: S02, S05, mod_arith

Leaf basis: mod_arith + forall_intro

For b=(2−a) mod 4: a*b≡a+(2−a)+1=3 (mod 4), and a*b lies between 0 and 3, so a*b=3=e; likewise b*a=3. Concretely: 0*2=3, 1*1=3, 2*0=3, 3*3=3, matching the table. Every element has an inverse.



S08 · impliesBefore

\text{closure, associativity, unique } e,\ \text{inverses}

After

(G,*)\ \text{is a group}

Conditions: none

Rule: group_axioms · Uses: S03, S04, S06, S07, group_axioms

Leaf basis: group_axioms + and_intro_elim

All four items of group qualification are proved (S03, S04, S06, S07), so by the group axioms (G,*) is a group. Only now does the second stage begin.



S09 · impliesBefore

a*b=(a+b+1)\bmod 4

After

a*b=(b+a+1)\bmod 4=b*a\ \text{for all } a,b\in G

Conditions: none

Rule: add_comm · Uses: S02, S08, add_comm

Leaf basis: add_comm + forall_intro

Integer addition is commutative, a+b+1=b+a+1, so a*b=b*a; a and b are arbitrary, covering all 16 pairs (including the 6 unordered off-diagonal pairs), not just a few samples. Equivalently, with rows and columns in the same order, the table is symmetric about its main diagonal; but this symmetry signals an abelian group only after the group qualification of S08.



S10 · impliesBefore

(G,*)\ \text{group},\ \forall a,b:\ a*b=b*a

After

(G,*)\ \text{is a finite abelian group of order } 4

Conditions: none

Rule: mko_fag · Uses: S08, S09, mko_fag

Leaf basis: mko_fag + and_intro_elim

Both stages pass: (G,*) is a group (S08) and all elements commute pairwise (S09). By the MKO, (G,*) is a finite abelian group of order |G|=4.



S11 · impliesBefore

0^1=0

After

0^2=0*0=1,\ 0^3=1*0=2,\ 0^4=2*0=3=e;\ \operatorname{ord}(0)=4

Conditions: none

Rule: power_def · Uses: S02, S05, power_def

Leaf basis: power_def + table_read

Compute with the same group operation, by the definition of powers: 0²=0*0=1, 0³=0²*0=1*0=2, 0⁴=0³*0=2*0=3=e. None of 0¹, 0², 0³ equals e=3, so the order of 0 is 4. The order must be computed relative to the identity 3, not the label 0 (MKO para1).



S12 · impliesBefore

\langle 0\rangle,\ 1^2=1*1

After

\langle 0\rangle=\{0,1,2,3\}=G;\ 1^2=3=e,\ \operatorname{ord}(1)=2,\ \langle 1\rangle=\{1,3\}

Conditions: none

Rule: power_def · Uses: S11, S02, S05, power_def

Leaf basis: power_def + table_read

The powers of 0 are 0, 1, 2, 3 and then repeat, so ⟨0⟩=G and the group defined by this table is cyclic. On the other hand 1¹=1≠e and 1²=1*1=3=e, so the order of 1 is 2 and ⟨1⟩={1,3}. The label 1 is not a generator; these subgroups belong only to this specified finite group (MKO para2).



S13 · impliesBefore

a\circ b=|a-b|\ \text{on}\ K=\{0,1,2\}

After

(1\circ 1)\circ 2=2\neq 0=1\circ(1\circ 2);\ (K,\circ)\ \text{is not a group}

Conditions: none

Rule: quantifier_negation · Uses: G3, abs_rules, quantifier_negation

Leaf basis: quantifier_negation + abs_rules + numeric_evaluation

Contrast table: |a−b|=|b−a|, so the table is symmetric about its diagonal; 0 is an identity (|0−b|=b); every element is its own inverse (a∘a=0). But (1∘1)∘2=0∘2=2 while 1∘(1∘2)=1∘1=0, so associativity fails. One counterexample refutes 'associative for all triples', so (K,∘) is not a group, and hence not an abelian group. A symmetric table cannot replace group qualification.







## Substeps and lemmas

S04.1 · impliesBefore

(a*b)*c=\big((a*b)+c+1\big)\bmod 4

After

(a*b)*c\equiv(a+b+1)+c+1=a+b+c+2\pmod 4

Conditions: none

Rule: mod_arith · Uses: S02, mod_arith, add_assoc

Leaf basis: mod_arith + add_assoc + add_comm

By the formula (a*b)*c=((a*b)+c+1) mod 4, it is congruent to (a*b)+c+1; also a*b≡a+b+1, and congruence is compatible with addition, so (a*b)*c≡a+b+1+c+1=a+b+c+2 (mod 4).



S04.2 · impliesBefore

a*(b*c)=\big(a+(b*c)+1\big)\bmod 4

After

a*(b*c)\equiv a+(b+c+1)+1=a+b+c+2\pmod 4

Conditions: none

Rule: mod_arith · Uses: S02, mod_arith, add_assoc

Leaf basis: mod_arith + add_assoc

Likewise, a*(b*c)≡a+(b*c)+1≡a+(b+c+1)+1=a+b+c+2 (mod 4).



S04.3 · impliesBefore

(a*b)*c\equiv a*(b*c)\pmod 4,\ \text{both in}\ \{0,1,2,3\}

After

(a*b)*c=a*(b*c)

Conditions: none

Rule: mod_arith · Uses: S04.1, S04.2, S03, mod_arith

Leaf basis: mod_arith

Transitivity of congruence gives (a*b)*c≡a*(b*c); by S03 both lie between 0 and 3, and two integers in this range that are congruent are equal.



S06.1 · impliesBefore

e,\ e'\ \text{two-sided identities}

After

e=e*e'=e'

Conditions: none

Rule: eq_refl_symm_trans · Uses: eq_refl_symm_trans

Leaf basis: eq_refl_symm_trans + def_unfold

Since e′ is an identity, e*e′=e; since e is an identity, e*e′=e′. By symmetry and transitivity of equality, e=e′. This proves Lemma L_id_unique, valid for any binary operation and without associativity.







## Reverse audits


- S13 · premise_audit · G3, abs_rules, quantifier_negation — A refutation needs one triple; it is not claimed that other triples fail too.
- S12 · premise_audit · S11, power_def, table_read — It needs the table values and e=3; no claim is made about any other group.
- S11 · premise_audit · S02, S05, power_def — It needs the table values and e=3; minimality comes from checking k=1, 2, 3 one by one.
- S10 · premise_audit · S08, S09, mko_fag — It only conjoins the two stages; the classification concerns this one supplied table.
- S09 · premise_audit · S02, S08, add_comm, forall_intro — It needs the formula valid for all a, b; checking only samples such as 0*1=1*0 and 0*2=2*0 would not be enough.
- S08 · premise_audit · S03, S04, S06, S07, group_axioms, and_intro_elim — None of the four items may be missing; commutativity has not been used yet.
- S07 · premise_audit · S02, S05, mod_arith — Inverses are taken relative to e=3 from S05; wrongly using the label 0 as the identity would give wrong inverses.
- S06.1 · premise_audit · eq_refl_symm_trans — It uses only the definition of the two identities and properties of equality; L_id_unique itself is not used.
- S06 · premise_audit · S05, L_id_unique — It needs existence from S05 and uniqueness from the lemma.
- S05 · premise_audit · S02, mod_arith, forall_intro — Both sides must be checked (left and right multiplication); this step checks both.
- S04.3 · premise_audit · S04.1, S04.2, S03, mod_arith — The key is that both sides are already remainders; numbers that are merely congruent, not both between 0 and 3, need not be equal.
- S04.2 · premise_audit · mod_arith, add_assoc — Symmetric to S04.1.
- S04.1 · premise_audit · mod_arith, add_assoc — Only properties of congruence and associativity of addition are used.
- S04 · premise_audit · S02, S03, mod_arith, forall_intro — It needs the formula of S02; a, b, c are arbitrary, so the conclusion is universal.
- S03 · premise_audit · S02, mod_arith — It needs the formula of S02 and the range of remainders; no converse is claimed.
- S02 · inverse_equivalence · table_read, mod_arith, G2 — The values of the formula on the 16 pairs are exactly the table; recomputing the table from the formula or reading the formula values off the table gives the same thing.
- S01 · premise_audit · mko_fag, group_axioms — This step only lists the obligations and derives no new fact.





## Error controls and negative controls

A symmetric table alone does not establish an abelian groupThe mistake named by the MKO is to declare an abelian group because the table is symmetric about its diagonal. The table of |a−b| is symmetric, has identity 0 and every element is self-inverse, yet (1∘1)∘2=2≠0=1∘(1∘2), so it is not a group (S13). Group qualification (S03 to S08) must be completed first; only then does commutativity classify anything.

A few commuting samples are not enoughAnother misconception identified in the MKO is to infer that the whole group commutes from a few commuting elements. S09 uses a formula valid for all a, b. A counterexample to the pattern: in the permutation group of {1,2,3}, r=(1 2 3) commutes with r² and the identity commutes with everything, but s=(1 2) does not commute with r: (r∘s)(1)=r(2)=3 while (s∘r)(1)=s(2)=1.

The identity need not be the label 0The labels 0 to n−1 are only names. The identity of this table is 3 (0*0=1≠0). Wrongly taking 0 as the identity gives wrong inverses and wrong orders: for example, the order of 0 would wrongly be taken as 1.


- The table of |a−b| on {0,1,2} is symmetric about the main diagonal, so it is an abelian group → reject — Associativity fails: (1∘1)∘2=2 and 1∘(1∘2)=0.
- From the two samples 0*1=1*0 and 0*2=2*0 one may infer that (G,*) is commutative → reject — Two samples do not cover the other four unordered off-diagonal pairs; the conclusion needs the argument of S09 for all a, b.
- The label 0 is the identity of this group → reject — 0*0=1≠0; the identity is 3.
- The element 1 generates the whole group G → reject — 1*1=3=e, so ⟨1⟩={1,3}≠G.





## Result and limitations

The given 4×4 table is a*b=(a+b+1) mod 4. It is closed, associative (both sides are congruent to a+b+c+2 modulo 4), has the unique identity e=3, every a has the inverse (2−a) mod 4, and it is commutative for all a, b, so (G,*) is a finite abelian group of order 4. The element 0 has order 4 and ⟨0⟩=G; the element 1 has order 2 and ⟨1⟩={1,3}. The symmetric contrast table |a−b| on {0,1,2} is not associative and is not a group.


- N1 to N9 are finite exhaustive checks over every element (or pair, or triple) of the carrier {0,1,2,3}. Since the carrier has exactly these four elements they cover every case of this one table; they cross-check the modular proofs of S03 to S09 and say nothing about other tables.
- The permutation-group counterexample in the error controls is not written as a complete 6×6 table; only one non-commuting pair is computed by composing permutations.





## Verification and source binding

17 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 8364c2e3fd58e2b9251219c8186c64a27ff0c6e88d59156b8ccb03f562a4beda
- original source SHA-256: 8364c2e3fd58e2b9251219c8186c64a27ff0c6e88d59156b8ccb03f562a4beda
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-abelian-group-01.json)