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

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

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

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

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

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

a,b\in G

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

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

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

3*b,\ a*3

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

e=3\ \text{is an identity}

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

a\in G

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

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

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

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

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

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

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

0^1=0

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

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

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

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

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

Substeps and lemmas

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

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

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

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

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

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

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

e=e*e'=e'

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 group

The 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 enough

Another 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 0

The 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)