Finite group: auditing the group axioms from a complete Cayley table

Goal and scope

Two complete operation tables are given. (A) For G={0,1,2,3} with table T, prove that (G,*) is a finite group: closure, associativity for all 4³=64 triples, a two-sided identity and two-sided inverses. (B) K={0,1,2} with table ∘ is symmetric, has a two-sided identity and two-sided inverses for every element, yet violates associativity at the triple (1,1,2), so it is not a group; also show that all 19 triples containing 0 pass, so sampling would misjudge it.

Treats only the specified finite models: elements labeled 0 to n−1 and the operation given by a complete n×n table (MKO assumption a1). Associativity is established by an argument covering every triple and cross-checked by enumerating all n³ triples (MKO assumption a2). Subgroups, homomorphisms and infinite groups are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• division_algorithm
• eq_refl_symm_trans
• case_analysis
• numeric_evaluation

• G1 — Candidate A: G={0,1,2,3}; row a of the table T lists a*0, a*1, a*2, a*3 in order: row 0 is 0,1,2,3; row 1 is 1,2,3,0; row 2 is 2,3,0,1; row 3 is 3,0,1,2.
• G2 — Candidate B: K={0,1,2}; row a of its table lists a∘0, a∘1, a∘2 in order: row 0 is 0,1,2; row 1 is 1,0,1; row 2 is 2,1,0.
• G3 — Sampled rows or a few triples do not prove a group; associativity must hold for every one of the n³ ordered triples (MKO assumption a2).

• G=\{0,1,2,3\} — the carrier of candidate A
• a*b — the entry of table T in row a, column b
• K=\{0,1,2\} — the carrier of candidate B
• a\circ b — the entry of table ∘ in row a, column b
• x\bmod m — the remainder of x on division by the positive integer m, 0≤r<m

Rules and sources

• division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
• 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.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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).
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• 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.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_finite_group_def · cited — Let a finite set G carry a binary operation *. If it is closed on G, associative for every triple, has a two-sided identity and every element has a two-sided inverse, then (G,*) is a finite group. A complete Cayley table allows exhaustive checking of the specified finite model. · mko-finite-group
• mod_notation · prerequisite — For an integer x and a positive integer m, x mod m denotes the remainder r of the division algorithm: the unique r with 0≤r<m and x=mq+r for some integer q.
• finite_exhaustion · prerequisite — On a finite set, a statement about all elements (or all ordered pairs or triples) holds exactly when it holds in each of the finitely many listed cases; checking every case is a complete proof for that finite model, but says nothing about other sets.
• L_same_rem · lemma — Let m be a positive integer and x, y integers. If x−y=mk for an integer k, then x mod m=y mod m.

Main derivation

(G,*)\ \text{given by table } T

\text{closure},\ \forall a,b,c:\ (a*b)*c=a*(b*c),\ \exists e\ \text{two-sided identity},\ \forall a\ \exists a'\ \text{two-sided inverse}

T(a,b)\ \text{for all } a,b\in G

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

a,b\in G

a*b\in G

x-y=mk,\ k\in\mathbb{Z}

x\bmod m=y\bmod m

(a*b)*c

(a+b+c)\bmod 4

a*(b*c)

(a+b+c)\bmod 4

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

\forall a,b,c\in G:\ (a*b)*c=a*(b*c)

\text{row } 0 \text{ and column } 0 \text{ of } T

\forall a\in G:\ 0*a=a\ \land\ a*0=a

a\in G

0'=0,\ 1'=3,\ 2'=2,\ 3'=1;\ a*a'=a'*a=0

\text{closure, associativity, identity, inverses}

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

(K,\circ)\ \text{given by its table}

\text{closed},\ a\circ b=b\circ a,\ 0\ \text{two-sided identity},\ a\circ a=0

(a,b,c)\in K^3,\ 0\in\{a,b,c\}

(a\circ b)\circ c=a\circ(b\circ c)

(1\circ 1)\circ 2\ \text{vs}\ 1\circ(1\circ 2)

0\circ 2=2\neq 0=1\circ 1

\exists (a,b,c):\ (a\circ b)\circ c\neq a\circ(b\circ c)

(K,\circ)\ \text{is not a group}

Substeps and lemmas

x\in\mathbb{Z},\ m>0

x=mq+r,\ 0\le r<m,\ r=x\bmod m

y=x-mk=m(q-k)+r,\ 0\le r<m

y\bmod m=r=x\bmod m

Reverse audits

• S14 · sufficient_goal_reduction · S13, quantifier_negation, mko_finite_group_def — Goal G: (K,∘) is not a group. Sufficient condition H: some triple violates associativity (H⇒G by the definition). H is read off the table in S13; G is never used as a premise.
• S13 · premise_audit · G2, def_unfold, numeric_evaluation — All four table lookups can be checked directly in G2; one counterexample suffices to refute the universal associativity law.
• S12 · premise_audit · S11, case_analysis — The three cases may overlap (for example two zeros), but all such triples are covered; the step claims nothing about the remaining 8 triples.
• S11 · premise_audit · G2, finite_exhaustion — Each property comes from cell-by-cell inspection; none of them involves triples, so they guarantee nothing about associativity.
• S10 · sufficient_goal_reduction · S03, S07, S08, S09, mko_finite_group_def — Goal G: (G,*) is a group. Sufficient condition H: the four conditions hold together; H⇒G by the definition. Each part of H is proved forwards from the table T; G is never used as a premise.
• S09 · premise_audit · G1, S08, finite_exhaustion — Inverses are defined relative to the identity of S08, and both products must give that same identity; all four elements are checked.
• S08 · premise_audit · G1, finite_exhaustion — Both the row and the column must be inspected; inspecting one side only yields a one-sided identity (see error control 3).
• S07 · premise_audit · S05, S06, eq_refl_symm_trans, forall_intro — ∀-introduction needs a, b, c to carry no special values, and in S05 and S06 they carry none. Associativity differs from commutativity; this step does not use a*b=b*a.
• S06 · inverse_equivalence · S02, L_same_rem, eq_replace — As in S05, this replaces equals by equals and holds both ways.
• S05 · inverse_equivalence · S02, L_same_rem, eq_replace — Both sides name the same integer; replacing equals by equals works in both directions.
• S04.2 · premise_audit · S04.1, division_algorithm, distributive — The key is uniqueness: without it, y might have another representation with a different remainder. The bound 0≤r<m is carried over from S04.1.
• S04.1 · premise_audit · division_algorithm, mod_notation — The division algorithm needs a positive divisor, which is what the condition m>0 provides.
• S04 · premise_audit · L_same_rem — The lemma needs m>0 and an integer k; only this direction is claimed. The converse (equal remainders imply the difference is a multiple of m) is also true but is neither needed nor used here.
• S03 · premise_audit · G1, finite_exhaustion, division_algorithm — Closure only requires every output to lie in G; on its own it gives neither associativity nor an identity.
• S02 · premise_audit · G1, finite_exhaustion, mod_notation — The formula is another description of the table, resting on all 16 cells matching; it holds for T only and does not claim that every table has such a formula.
• S01 · premise_audit · G1, mko_finite_group_def — This step only lists the conditions to check and derives no new fact. None of the four may be skipped; they are checked one by one below.

Error controls and negative controls

A symmetric table is not thereby a group

The MKO names the mistake of declaring a group from the symmetry of the table. Symmetry means only commutativity, which is not a group axiom and does not imply associativity. Candidate B's table is fully symmetric with an identity and inverses, yet violates associativity at (1,1,2).

Sampling triples is not enough

Of the 27 triples of candidate B, the 19 containing 0 all pass (S12). A sample of a few triples may well fall entirely among those 19 and mislead. Associativity must cover all n³ triples: for candidate A this guide does so with an argument valid for arbitrary a, b, c (S05 to S07) and cross-checks by enumerating all 64 triples in N4.

One-sided identity or inverse

The MKO also warns against treating a one-sided identity or inverse as two-sided. Example: on {0,1,2} let a•b=(a−b) mod 3. For every a, a•0=a, so 0 is a right identity; but 0•1=2≠1, so 0 is not a left identity and there is no two-sided identity. S08 must inspect both row 0 and column 0, and S09 both a*a' and a'*a.

• Candidate B's table is symmetric and has an identity and inverses, so (K,∘) is a group → reject — Associativity fails at (1,1,2): (1∘1)∘2=2 while 1∘(1∘2)=0.
• The triples (0,1,2), (1,0,2), (2,1,0) and (1,2,0) are all associative, so ∘ is associative → reject — All four contain 0 and pass automatically; (1,1,2), which avoids 0, fails. Establishing associativity requires an argument covering all 27 triples.
• On {0,1,2} with a•b=(a−b) mod 3, 0 is the identity because a•0=a for every a → reject — 0 is only a right identity: 0•1=2≠1.
• Any table whose rows and columns are permutations of the set (a Latin square) defines a group → reject — The table of (a−b) mod 3 is a Latin square, but (0•1)•1=2•1=1 while 0•(1•1)=0•0=0.

Result and limitations

The table of candidate A (G,*) is a*b=(a+b) mod 4; it is closed, all 64 triples are associative, 0 is a two-sided identity, and the two-sided inverses of 0, 1, 2, 3 are 0, 3, 2, 1, so it is a finite group. Candidate B (K,∘) is closed, symmetric, has 0 as a two-sided identity and every element is its own inverse, and the 19 triples containing 0 are associative, but (1∘1)∘2=2≠0=1∘(1∘2), so it is not a group.

• The conclusions concern only the two specified finite models (MKO assumption a2); subgroups, homomorphisms, cosets and so on (the MKO's formal next) are not treated.
• N4 is a finite enumeration of all 64 triples of candidate A, complete for this model, but it relies on the formula of S02 reproducing table T; the argument of S05 to S07 does not depend on N4.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: df045187fbff83ea6ba906772f9d4bccd3acd1bc60dcb87c4028857733f76d42
• original source SHA-256: df045187fbff83ea6ba906772f9d4bccd3acd1bc60dcb87c4028857733f76d42
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)