Finite commutative ring: checking commutativity of ℤ₆ over all element pairs, with an upper-triangular matrix ring as a non-commutative counterexample

Goal and scope

(1) On ℤ₆={0,1,2,3,4,5} (a⊕b=(a+b) mod 6, a⊗b=(ab) mod 6), already qualified as a finite unital ring, check a⊗b=b⊗a for all 36 ordered element pairs and decide whether ℤ₆ is a finite commutative ring. (2) Show that ℤ₆ has nonzero zero divisors and that 2 is not invertible, so it is neither an integral domain nor a field. (3) In the qualified ring U of 2-by-2 upper-triangular matrices over 𝔽₂, show that several products commute and yet U is not commutative.

Works inside the MKO's scope: it uses the same addition and multiplication tables of rings already qualified as finite unital rings (assumption a1), and does not recheck the ring axioms; commutativity quantifies over every ordered element pair, with no extra premise of no zero divisors or invertibility of nonzero elements (assumption a2). Integral domains and fields appear only to show that a commutative ring need not have these properties. The canonical MKO and its English edition are not changed.

Givens and symbols

• mul_comm
• eq_refl_symm_trans
• matrix_product_def
• quantifier_negation
• numeric_evaluation

• G1 — ℤ₆ has carrier {0,1,2,3,4,5}, a⊕b=(a+b) mod 6 and a⊗b=(ab) mod 6. The rows of the multiplication table are: row 0 (0,0,0,0,0,0); row 1 (0,1,2,3,4,5); row 2 (0,2,4,0,2,4); row 3 (0,3,0,3,0,3); row 4 (0,4,2,0,4,2); row 5 (0,5,4,3,2,1); the entry at column index b in row a is a⊗b.
• G2 — (ℤ₆,⊕,⊗) has already qualified, with these two complete tables, as a finite unital ring in the parent node, with additive identity 0 and multiplicative identity 1; this guide does not recheck it.
• G3 — U has as carrier the 8 triples (a,b,c)∈{0,1}³, standing for the matrix with first row (a,b) and second row (0,c); addition is entrywise mod 2 and multiplication is the matrix product mod 2. U has already qualified as a finite unital ring in the parent node, with identity I=(1,0,1); this guide does not recheck it.

• \mathbb{Z}_6=\{0,1,2,3,4,5\} — the carrier of residues mod 6
• a\otimes b=(ab)\bmod 6 — the multiplication table of ℤ₆
• U — the ring of 2-by-2 upper-triangular matrices over 𝔽₂, elements written (a,b,c)
• (a,b,c) — stands for the matrix with first row (a,b) and second row (0,c)
• E_{11},E_{12},E_{22},I — the elements (1,0,0), (0,1,0), (0,0,1), (1,0,1) of U

Rules and sources

• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• 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.
• matrix_product_def · prerequisite — Matrix product: for A of size m×n and B of size n×p, (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}. Matrix multiplication is in general not commutative.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• 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.
• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• 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.
• 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.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• add_zero · prerequisite — Additive identity: u+0=u.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_comm_ring_def · cited — Using the same complete addition and multiplication tables of an already qualified finite unital ring, require a*b=b*a for every a,b. All element pairs are checked rather than guessed from a few samples or apparent table symmetry. · mko-finite-commutative-ring
• mko_unital_ring_def · cited — Complete addition and multiplication tables on one finite carrier: addition forms an abelian group; multiplication is associative and distributes over addition on both sides; there is a unique multiplicative identity 1 with 1≠0. Commutativity of multiplication is not required. · mko-finite-unital-ring
• mod_reduce · prerequisite — For an integer m and a positive integer n, m mod n is the unique integer r with 0≤r<n such that n divides m−r; equal integers have equal residues.
• domain_field_def · prerequisite — Nonzero elements a, b with ab=0 are zero divisors. An integral domain is a commutative ring with 1≠0 and no zero divisors; a field is a commutative ring in which every nonzero element has a multiplicative inverse.

Main derivation

\mathbb{Z}_6\ \text{finite commutative ring}

\mathbb{Z}_6\ \text{qualified unital ring}\ \land\ \forall a,b\in\mathbb{Z}_6:\ a\otimes b=b\otimes a

\mathbb{Z}_6\times\mathbb{Z}_6

36=6\ \text{diagonal pairs}+30\ \text{off-diagonal pairs}

(a,a),\ a\in\mathbb{Z}_6

a\otimes a=a\otimes a

a\otimes b=b\otimes a\ \ \text{and}\ \ b\otimes a=a\otimes b

\text{one equation per group}\ \{a,b\},\ a<b:\ 15\ \text{checks}

a\otimes b=(ab)\bmod 6

a\otimes b=(ab)\bmod 6=(ba)\bmod 6=b\otimes a\ \ (\forall a,b\in\mathbb{Z}_6)

\text{row}\ a\ \text{vs. column}\ a\ \text{of the listed table}

\text{the 15 entries above the diagonal equal the 15 below}

\text{6 diagonal pairs (S03)},\ \text{30 off-diagonal pairs (S05, S06)}

\mathbb{Z}_6\ \text{is a finite commutative ring}

2\otimes 3=(6)\bmod 6

2\otimes 3=0,\ 2\neq 0,\ 3\neq 0\ \Rightarrow\ \mathbb{Z}_6\ \text{not an integral domain}

\text{row 2}=(0,2,4,0,2,4)

\nexists x:\ 2\otimes x=1\ \Rightarrow\ \mathbb{Z}_6\ \text{not a field}

\begin{pmatrix}a&b\\0&c\end{pmatrix}\begin{pmatrix}a'&b'\\0&c'\end{pmatrix}

(a,b,c)(a',b',c')=(aa',\ ab'+bc',\ cc')\bmod 2

E_{11}E_{12}=(1,0,0)(0,1,0)

E_{11}E_{12}=(1\cdot0,\ 1\cdot1+0\cdot0,\ 0\cdot0)=(0,1,0)=E_{12}

E_{12}E_{11}=(0,1,0)(1,0,0)

E_{12}E_{11}=(0\cdot1,\ 0\cdot0+1\cdot0,\ 0\cdot0)=(0,0,0)

E_{11}E_{12}=(0,1,0)\neq(0,0,0)=E_{12}E_{11}

\exists a,b\in U:\ ab\neq ba\ \Rightarrow\ U\ \text{not commutative}

IX=XI,\ E_{11}E_{22}=(0,0,0)=E_{22}E_{11},\ E_{11}E_{11}=E_{11}

\text{some pairs commute, yet}\ U\ \text{is not commutative}

\text{S07},\ \text{S08},\ \text{S09},\ \text{S13}

\mathbb{Z}_6\ \text{commutative, not a domain, not a field};\ U\ \text{not commutative}

Substeps and lemmas

No substeps in this guide.

Reverse audits

• S15 · sufficient_goal_reduction · S07, S08, S09, S13, and_intro_elim — Goal G is the conjunction of the three tasks; H is proved forwards by S07, S08, S09 and S13, H⇒G by conjunction introduction, and G is never used as a premise.
• S14 · premise_audit · S10, S13, numeric_evaluation — The commuting samples do not contradict S13: a universal statement is refuted by one counterexample and is not proved by positive samples that leave cases unexamined (N8). For a finite domain, a successful exhaustive check of all ordered pairs does establish that finite universal statement.
• S13 · premise_audit · S11, S12, quantifier_negation — Refuting a universal statement needs one witness; this does not affect U's qualification as a unital ring (G3).
• S12 · inverse_equivalence · S10, numeric_evaluation — Exact computation; both sides are the same element (N7).
• S11 · inverse_equivalence · S10, numeric_evaluation — Exact computation; both sides are the same element (N6).
• S10 · inverse_equivalence · matrix_product_def, mul_zero — Triples correspond one-to-one to upper-triangular matrices, and the formula is another way of writing the same product, so the step holds both ways.
• S09 · premise_audit · G1, domain_field_def — Denying existence needs every x to be checked; row 2 lists the values for all six x (N5 recomputes over the whole carrier).
• S08 · premise_audit · G1, domain_field_def, numeric_evaluation — One pair of zero divisors suffices to deny the integral-domain property (N4); commutativity itself is not denied.
• S07 · sufficient_goal_reduction · S01, S02, S03, S05, case_analysis — Goal G: ℤ₆ is commutative. Sufficient condition H: parent qualification and all 36 pairs commute; H⇒G by the definition in S01. H is proved forwards from G2, S03 and S05, without using G.
• S06 · premise_audit · G1, S04, case_analysis — The 15 groups cover every off-diagonal ordered pair (S02, S04); N3 recomputes the formula at all 36 pairs, and since the carrier is exactly these six elements this finite check exhausts every pair.
• S05 · premise_audit · mul_comm, mod_reduce, G1 — The formula certificate uses the operation explicitly defined by G1 as (ab) mod 6. S06 separately checks the 15 off-diagonal symmetry equations of the listed table. It establishes table symmetry, not equality of all 36 stored entries with the formula; transferring a formula certificate to an arbitrary independent table would require that additional consistency check.
• S04 · inverse_equivalence · eq_refl_symm_trans — Symmetry of equality works both ways, so the two conditions are true or false together.
• S03 · premise_audit · eq_refl_symm_trans — Only reflexivity is used; these 6 pairs need no ring property.
• S02 · inverse_equivalence · finite_counting_basics, numeric_evaluation — Diagonal and off-diagonal form a disjoint and exhaustive split, 6+30=36, so both sides describe the same set (N1, N2).
• S01 · premise_audit · G2, mko_comm_ring_def, mko_unital_ring_def — This step only unfolds the definition; if the parent qualification failed, a symmetric table would still not make a commutative ring.

Error controls and negative controls

Commuting samples do not prove commutativity

The misconception identified in the MKO is to declare a ring commutative after seeing several commuting products. In U the identity, E₁₁ with E₂₂, and every element with itself commute, but E₁₁E₁₂≠E₁₂E₁₁. Commutativity must quantify over every ordered pair: for ℤ₆ the formula certificate plus 15 equations cover all 36 pairs.

A commutative ring is not automatically a domain or field

Another misconception identified in the MKO is to treat a commutative ring as an integral domain or field. ℤ₆ is commutative, but 2⊗3=0 (zero divisors) and 2 is not invertible. Commutativity only says ab=ba; it does not say that ab=0 forces a=0 or b=0, and it supplies no inverses.

Apparent symmetry must be checked entry by entry

Seeing that a table looks roughly symmetric is not enough; one miscopied entry would change the conclusion. This guide uses two independent routes: the formula certificate of S05 and the group-by-group check of the 15 equations on the listed table in S06; N3 recomputes the formula at all 36 pairs.

• In U, I commutes with everything and E₁₁ commutes with E₂₂, so U is commutative → reject — E₁₁E₁₂=E₁₂ while E₁₂E₁₁=0, and these differ.
• ℤ₆ is a commutative ring, so it has no zero divisors → reject — 2⊗3=0 with both 2 and 3 nonzero.
• ℤ₆ is a finite commutative ring, so every nonzero element is invertible → reject — Row 2, (0,2,4,0,2,4), contains no 1, so 2 is not invertible.
• If one row of the multiplication table equals the corresponding column, the ring is commutative → reject — In U the row and column of the identity I agree, yet U is not commutative; every row must equal its column.

Result and limitations

Multiplication in ℤ₆ commutes for all 36 ordered pairs (the 6 diagonal pairs by reflexivity, the 30 off-diagonal pairs by 15 equations and the formula certificate), so ℤ₆ is a finite commutative ring; but 2⊗3=0 and 2 has no multiplicative inverse, so it is neither an integral domain nor a field. In the upper-triangular matrix ring U over 𝔽₂, samples such as I, E₁₁, E₂₂ commute, but E₁₁E₁₂=E₁₂≠0=E₁₂E₁₁, so U is not commutative.

• The finite-unital-ring qualifications of ℤ₆ and U are taken from the parent node (G2, G3); this guide does not recheck the ring axioms.
• The complete 8-by-8 multiplication table of U is generated by the formula of S10; the guide does not print every cell and computes only the products it uses.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 71ebaf592c6af1889ee73c2b6cda7d5ccfdbf9107995322905339d85c5f7b990
• original source SHA-256: 2aae99393024c2da54cb50cf7b82689e6617f3ce5fb9975a73db4ae5405b5182
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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