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

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

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-unital-ring-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

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

After

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

Conditions: none

Rule: mko_ring_def · Uses: G1, G2

Leaf basis: mko_ring_def + def_unfold

List every obligation from the MKO: addition is an abelian group (closure, associativity, identity 0, inverses, commutativity); multiplication is associative; left and right distributivity are checked separately; there is a unique two-sided multiplicative identity 1, and 1≠0. Commutativity of multiplication is not an obligation.



S02 · impliesBefore

\text{the 32 entries of the two tables}

After

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

Conditions: none

Rule: finite_forall · Uses: G1, G2, G3, finite_forall

Leaf basis: finite_forall + division_algorithm + numeric_evaluation

Compare the 16+16 table entries with the formulas cell by cell. For example row 3 of ⊙: 3·0=0, 3·1=3, 3·2=6 with remainder 2, 3·3=9 with remainder 1, matching 0,3,2,1 in the table; row 2: 0, 2, 4 with remainder 0, 6 with remainder 2; row 3 of ⊕: 3, 4 with remainder 0, 5 with remainder 1, 6 with remainder 2. All 32 cells agree, so the two table operations are exactly addition and multiplication mod 4.



S03 · theorem_applicationBefore

m,\ k\in\mathbb{Z}

After

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

Conditions: none

Rule: L_mod_compat · Uses: G3

Leaf basis: L_mod_compat

Lemma L_mod_compat (proved in S03.1 to S03.3) says that reducing, operating and reducing again gives the same as operating and then reducing. Every axiom below is reduced to the corresponding identity of integers.



S04 · impliesBefore

a,b\in X

After

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

Conditions: none

Rule: division_algorithm · Uses: S02, G3

Leaf basis: division_algorithm

A remainder satisfies 0≤r<4, so every result lies in X: both operations are closed binary operations on X. Also, for a∈X, a=4·0+a with 0≤a<4, so r(a)=a by uniqueness; this is used below to replace c by r(c).



S05 · equivalentBefore

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

After

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

Conditions: a,b,c\in X

Rule: L_mod_compat · Uses: S02, S03, S04

Leaf basis: L_mod_compat + add_assoc + add_comm + forall_intro

Since c=r(c), r(r(a+b)+c)=r(r(a+b)+r(c))=r((a+b)+c) by the lemma. Likewise a⊕(b⊕c)=r(a+r(b+c))=r(a+(b+c)). Integer addition is associative, so the two agree: ⊕ is associative. Also r(a+b)=r(b+a), so ⊕ is commutative. a, b, c are arbitrary elements of X, so all 64 triples are covered.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: group_axioms · Uses: S02, S04, G1

Leaf basis: group_axioms + finite_forall + numeric_evaluation

a⊕0=r(a)=a and 0⊕a=a, so 0 is the additive identity (row 0 and column 0 of the addition table are 0,1,2,3). Inverses: 1⊕3=r(4)=0, 2⊕2=r(4)=0, 3⊕1=0, 0⊕0=0; each row of the addition table contains exactly one 0. So every element has an additive inverse.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: group_axioms · Uses: S04, S05, S06

Leaf basis: group_axioms + and_intro_elim

Combining S04 (closure), S05 (associativity, commutativity) and S06 (identity, inverses), (X,⊕) is an abelian group with additive identity 0.



S08 · equivalentBefore

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

After

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

Conditions: a,b,c\in X

Rule: L_mod_compat · Uses: S02, S03, S04

Leaf basis: L_mod_compat + mul_assoc + forall_intro

Since c=r(c), r(r(ab)c)=r(r(ab)r(c))=r((ab)c) by the lemma; a⊙(b⊙c)=r(a·r(bc))=r(r(a)r(bc))=r(a(bc)). Integer multiplication is associative, so ⊙ is associative, for every triple.



S09 · equivalentBefore

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

After

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

Conditions: a,b,c\in X

Rule: L_mod_compat · Uses: S02, S03, S04

Leaf basis: L_mod_compat + distributive + forall_intro

Left distributivity: r(a·r(b+c))=r(r(a)r(b+c))=r(a(b+c))=r(ab+ac)=r(r(ab)+r(ac))=(a⊙b)⊕(a⊙c). The second equality and the last use the multiplicative and additive parts of the lemma; the middle uses integer distributivity.



S10 · equivalentBefore

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

After

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

Conditions: a,b,c\in X

Rule: L_mod_compat · Uses: S02, S03, S04

Leaf basis: L_mod_compat + distributive + forall_intro

The right law is proved separately: r(r(a+b)c)=r(r(a+b)r(c))=r((a+b)c)=r(ac+bc)=r(r(ac)+r(bc))=(a⊙c)⊕(b⊙c). It uses integer right distributivity (a+b)c=ac+bc and does not borrow commutativity of ⊙.



S11 · impliesBefore

1\odot a,\ a\odot 1

After

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

Conditions: none

Rule: mul_one · Uses: S02, S04, G2

Leaf basis: mul_one + finite_forall

1⊙a=r(a)=a and a⊙1=r(a)=a; row 1 and column 1 of the multiplication table are both 0,1,2,3. So 1 is a two-sided multiplicative identity (the MKO requires it to act on both sides).



S12 · theorem_applicationBefore

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

After

e=1

Conditions: none

Rule: L_unique_identity · Uses: S11

Leaf basis: L_unique_identity

By Lemma L_unique_identity (proved in S12.1), any two-sided identity e equals 1, so the multiplicative identity is unique. The table agrees: only row 1 equals 0,1,2,3.



S13 · impliesBefore

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

After

1\neq 0

Conditions: none

Rule: numeric_evaluation · Uses: S06, S11

Leaf basis: numeric_evaluation + mul_one

1 and 0 are different elements of X, and they act differently: 1⊙1=1 while 0⊙1=0. The MKO requires 1≠0, which rules out the one-element zero ring.



S14 · impliesBefore

\text{all obligations of S01}

After

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

Conditions: none

Rule: mko_ring_def · Uses: S01, S07, S08, S09, S10, S11, S12, S13

Leaf basis: mko_ring_def + and_intro_elim

Every obligation of S01 is proved: S07 (additive abelian group), S08 (associative multiplication), S09 and S10 (both distributive laws), S11 to S13 (unique two-sided identity with 1≠0). So it is a finite unital ring. Also 2⊙2=r(4)=0 with 2≠0, so 2 is a zero divisor: the ring is not an integral domain or a field, but the MKO does not require those (they are separate nodes).







## Substeps and lemmas

S03.1 · impliesBefore

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

After

r(m)=r(m')

Conditions: 0\le r(m')<4

Rule: division_algorithm · Uses: G3, division_algorithm

Leaf basis: division_algorithm + distributive + add_assoc

First an auxiliary fact: if m−m′ is a multiple of 4, the two have the same remainder. From m′=4s+r(m′) we get m=m′+4t=4(s+t)+r(m′) with 0≤r(m′)<4. Uniqueness in the division algorithm says the remainder of m can only be r(m′).



S03.2 · impliesBefore

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

After

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

Conditions: none

Rule: distributive · Uses: S03.1, G3

Leaf basis: distributive + add_assoc + add_comm

Adding gives m+k=4(q+p)+(r(m)+r(k)), so m+k and r(m)+r(k) differ by a multiple of 4; by S03.1 they have the same remainder. N3 checks the algebraic identity used.



S03.3 · impliesBefore

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

After

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

Conditions: none

Rule: distributive · Uses: S03.1, G3

Leaf basis: distributive + mul_comm + mul_assoc + add_assoc

Expand mk=(4q+r(m))(4p+r(k))=16qp+4q·r(k)+4p·r(m)+r(m)r(k), so mk and r(m)r(k) differ by 4(4qp+q·r(k)+p·r(m)), a multiple of 4; by S03.1 the remainders agree. S03.1 to S03.3 together prove Lemma L_mod_compat. N2 checks the expansion.



S12.1 · impliesBefore

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

After

e=e\odot e'=e'

Conditions: none

Rule: eq_refl_symm_trans · Uses: eq_refl_symm_trans

Leaf basis: eq_refl_symm_trans + eq_replace

e′ is a right identity, so e⊙e′=e; e is a left identity, so e⊙e′=e′. Symmetry and transitivity of equality give e=e′. This proves Lemma L_unique_identity.







## 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 ringOne 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 enoughThe ⊙′ 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 requiredThe 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-unital-ring-01.json)