Finite unital ring: proving that the mod-4 addition and multiplication tables form a unital ring

Goal and scope

On the carrier X={0,1,2,3}, complete addition and multiplication tables ⊕ and ⊙ (addition and multiplication mod 4) are given. Prove for all pairs and triples: (X,⊕) is an abelian group; ⊙ is associative; ⊙ distributes over ⊕ on both sides; there is a unique two-sided multiplicative identity 1, and 1≠0. Note also that 2⊙2=0 does not stop it from being a unital ring.

Stays inside the MKO: carrier labels 0 to 3 and two complete 4×4 tables (assumption a1); qualification holds exactly for every pair and triple (assumption a2). The main proof first checks that the 32 table entries equal the mod-4 formulas, then proves the axioms for all triples at once with a lemma on compatibility of remainders; N4 to N7 add an exhaustive cross-check over all 64 triples. Commutativity of multiplication is not required, and integral domains, fields, ideals and quotient rings are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• division_algorithm
• group_axioms
• distributive
• finite_forall

• G1 — Addition table ⊕ (row a, column b): 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 — Multiplication table ⊙ (row a, column b): row 0 is 0,0,0,0; row 1 is 0,1,2,3; row 2 is 0,2,0,2; row 3 is 0,3,2,1.
• G3 — r(m) is the remainder of the integer m on division by 4: by the division algorithm m=4q+r(m) with 0≤r(m)<4, and q, r(m) are unique.

• X — carrier {0,1,2,3}
• a\oplus b,\ a\odot b — the operations given by the addition and multiplication tables
• r(m) — remainder of the integer m on division by 4, 0≤r(m)<4
• 0,\ 1 — additive identity and multiplicative identity
• \ominus a — additive inverse of a

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.
• 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.
• 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.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• 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.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• 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.
• 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.
• mko_ring_def · cited — Supply complete addition and multiplication tables on the same finite carrier X. Addition must form an abelian group; multiplication must be associative and distribute over addition on both sides. There must be a unique multiplicative identity 1, distinct from the additive identity 0. This slice does not require multiplication to commute. · mko-finite-unital-ring
• finite_forall · prerequisite — Finite universal: for a finite set D, 'for all t∈D, Φ(t)' is equivalent to the conjunction of the instances obtained by substituting each element of D; the list must be complete.
• L_mod_compat · lemma — For all integers m and k: r(m+k)=r(r(m)+r(k)) and r(mk)=r(r(m)r(k)).
• L_unique_identity · lemma — If e and e′ are both two-sided identities for ⊙, then e=e′.

Main derivation

(X,\oplus,\odot)\ \text{finite unital ring}

(X,\oplus)\ \text{abelian group};\ \odot\ \text{associative};\ \text{left and right distributive};\ \exists!\,1,\ 1\neq 0

\text{the 32 entries of the two tables}

a\oplus b=r(a+b),\ a\odot b=r(ab)\ \text{for all}\ a,b\in X

m,\ k\in\mathbb{Z}

r(m+k)=r(r(m)+r(k)),\ r(mk)=r(r(m)r(k))

a,b\in X

a\oplus b\in X,\ a\odot b\in X,\ r(a)=a

(a\oplus b)\oplus c=r(r(a+b)+c)

r(a+b+c)=a\oplus(b\oplus c),\quad a\oplus b=b\oplus a

a\oplus 0,\ a\oplus(\ominus a)

a\oplus 0=a;\ \ominus0=0,\ \ominus1=3,\ \ominus2=2,\ \ominus3=1

\text{closure, associativity, identity 0, inverses, commutativity}

(X,\oplus)\ \text{abelian group}

(a\odot b)\odot c=r(r(ab)\,c)

r(abc)=a\odot(b\odot c)

a\odot(b\oplus c)=r(a\,r(b+c))

r(ab+ac)=(a\odot b)\oplus(a\odot c)

(a\oplus b)\odot c=r(r(a+b)\,c)

r(ac+bc)=(a\odot c)\oplus(b\odot c)

1\odot a,\ a\odot 1

1\odot a=a=a\odot 1\ \text{for all}\ a\in X

e\ \text{a two-sided identity for}\ \odot

e=1

0\ \text{additive identity},\ 1\ \text{multiplicative identity}

1\neq 0

\text{all obligations of S01}

(X,\oplus,\odot)\ \text{is a finite unital ring};\ 2\odot2=0

Substeps and lemmas

m-m'=4t,\ m'=4s+r(m')

r(m)=r(m')

m=4q+r(m),\ k=4p+r(k)

(m+k)-(r(m)+r(k))=4(q+p)\Rightarrow r(m+k)=r(r(m)+r(k))

m=4q+r(m),\ k=4p+r(k)

mk-r(m)r(k)=4(4qp+q\,r(k)+p\,r(m))\Rightarrow r(mk)=r(r(m)r(k))

e\odot x=x=x\odot e,\ e'\odot x=x=x\odot e'\ \forall x

e=e\odot e'=e'

Reverse audits

• S14 · sufficient_goal_reduction · S01, S07, S08, S09, S10, S11, S12, S13 — Goal G: a unital ring. Sufficient condition H: all obligations of S01; H⇒G by the definition. H is proved forwards in S02 to S13; G is never used as a premise.
• S13 · premise_audit · S06, S11 — It needs only a comparison of two elements and no other axiom.
• S12.1 · premise_audit · eq_refl_symm_trans — It uses that one is a left identity and the other a right identity; this sub-step does not use L_unique_identity.
• S12 · premise_audit · S11, L_unique_identity — It needs 1 itself to be a two-sided identity (S11); uniqueness does not depend on the size of the table.
• S11 · premise_audit · S04, G2, mul_one — Both the row and the column are checked, so it is two-sided; one side alone would not suffice.
• S10 · inverse_equivalence · L_mod_compat, distributive — The chain can be reversed; this guide directly proves each distributive law without using multiplicative commutativity; the noncommutative matrix example is not used to infer logical independence.
• S09 · inverse_equivalence · L_mod_compat, distributive — The chain can be reversed; only the left law is proved here, the right law separately in S10.
• S08 · inverse_equivalence · L_mod_compat, S04, mul_assoc — Every link of the chain is a rewrite of equal values and can be reversed.
• S07 · sufficient_goal_reduction · S04, S05, S06, group_axioms — Goal: addition is an abelian group. Sufficient condition: the group axioms plus commutativity, all proved forwards in the preceding steps.
• S06 · premise_audit · S04, G1, group_axioms — The inverses of all four elements are listed; since ⊕ is commutative, one-sided means two-sided.
• S05 · inverse_equivalence · L_mod_compat, S04, add_assoc — Every equality is a rewrite of equal values (the lemma is an equation), so the chain reads backwards as well.
• S04 · premise_audit · S02, division_algorithm — Closure needs only that values lie in X; r(a)=a is claimed only for a in X.
• S03.3 · premise_audit · S03.1, distributive — It uses only distributivity and commutativity of integers and S03.1; this sub-step does not use L_mod_compat.
• S03.2 · premise_audit · S03.1, distributive — It uses only distributivity of integers and S03.1; this sub-step does not use L_mod_compat.
• S03.1 · premise_audit · division_algorithm — The key is uniqueness: one representation with 0≤r<4 fixes the remainder. This sub-step does not use L_mod_compat.
• S03 · premise_audit · G3, L_mod_compat — It relies only on existence and uniqueness in the division algorithm; it holds for all integers, not a finite sample.
• S02 · premise_audit · G1, G2, G3, finite_forall — All 32 cells are compared, so this is a complete check over every pair, not a sample; the axiom proofs below rest on this identification.
• S01 · premise_audit · mko_ring_def — This step only unfolds the definition and derives no new fact.

Error controls and negative controls

Having a multiplicative identity is not being a ring

One mistake named by the MKO is to take a finite table that merely has a multiplicative identity as a unital ring. On the same ⊕, let ⊙′ be the minimum for the order 0<2<3<1: 1 is an identity for ⊙′, and ⊙′ is associative and commutative, but 2⊙′(1⊕1)=2⊙′2=2 while (2⊙′1)⊕(2⊙′1)=2⊕2=0, so distributivity fails.

Distributivity samples are not enough

The ⊙′ above passes all 32 left-distributivity triples with a=0 or a=1 (both sides are 0 when a=0, and 1 is the identity when a=1), yet fails at (2,1,1). So the law must hold for every triple; this guide proves all 64 triples at once with the lemma, and N4 to N7 check them exhaustively.

Check both distributive laws; commutativity is not required

The MKO does not require commutative multiplication. For example 2×2 matrices over ℤ/2 have 16 elements and E11·E12=E12 but E12·E11=0, illustrating noncommutativity. That matrix ring satisfies both distributive laws, so it is not an example with one law true and the other false. This guide keeps the two laws as separate proof obligations, directly verified in S09 and S10; S10 uses no commutativity. No logical-independence theorem for distributive axioms is claimed here.

• The one-point carrier {0} with 0⊕0=0 and 0⊙0=0 is a unital ring in the sense of this MKO → reject — The only possible multiplicative identity is 0, but the MKO requires 1≠0.
• The mod-4 tables are not a unital ring because 2⊙2=0 → reject — A unital ring need not be free of zero divisors; S14 shows every obligation holds.
• The multiplication of a unital ring must be commutative → reject — 2×2 matrices over ℤ/2 form a unital ring, but E11·E12=E12≠0=E12·E11.
• (X,⊕,⊙′), with ⊙′ the minimum for the order 0<2<3<1, has identity 1 and passes the distributivity samples with a=0, 1, so it is a unital ring → reject — 2⊙′(1⊕1)=2 while (2⊙′1)⊕(2⊙′1)=0.

Result and limitations

The two tables on X={0,1,2,3} are exactly addition and multiplication mod 4; by the remainder-compatibility lemma, (X,⊕) is an abelian group, ⊙ is associative and distributes on both sides, and 1 is the unique two-sided multiplicative identity with 1≠0. So it is a finite unital ring; 2⊙2=0 shows it has zero divisors, which does not violate the definition.

• N4 to N7 evaluate the mod-4 formulas at all 64 triples of X; they are an exhaustive cross-check valid for this carrier only and rely on the cell-by-cell identification of tables and formulas in S02.
• The ring axioms for the 2×2 matrix ring in the error controls are not proved here; it only illustrates that commutativity is not part of the definition.

Verification and source binding

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

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

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