# Finite two-sided ideal: checking left and right absorption separately in an upper-triangular matrix ring [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-finite-two-sided-ideal/) 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-two-sided-ideal-01 · production-20261019-adopted-96 ## Goal and scope The parent ring U is the ring of 2-by-2 upper-triangular matrices over 𝔽₂ (elements written (a,b,c) for the matrix with first row (a,b) and second row (0,c)), already qualified as a finite unital ring. (1) Prove that I={(0,0,0),(0,1,0)} is a two-sided ideal of U. (2) Prove that L={(0,0,0),(1,0,0)} satisfies left absorption but is not a two-sided ideal. (3) Prove that the diagonal subring D={(a,0,c)} contains 1 but is not an ideal. (4) Show that {0} and U itself are two-sided ideals. Works inside the MKO's scope: the parent ring qualifies as a finite unital ring with both complete tables, and each candidate subset is fully listed by distinct carrier elements (assumption a1); left and right absorption are quantified separately and checked by formula certificates valid for every element of the parent ring, not by sampling (assumption a2). Quotient rings (the next node) are not treated, the parent ring's axioms are not rechecked, and the canonical MKO and its English edition are not changed. ## Givens and symbols - matrix_product_def - mul_zero - and_intro_elim - quantifier_negation - numeric_evaluation - G1 — U has as carrier the 8 triples (a,b,c)∈{0,1}³; addition is entrywise mod 2; multiplication is (a,b,c)(a',b',c')=(aa', ab'+bc', cc') mod 2 (from the matrix product). The zero is (0,0,0) and the identity is 1_U=(1,0,1). - G2 — U has already qualified, with its complete addition and multiplication tables, as a finite unital ring in the parent node; this guide does not recheck the ring axioms. - G3 — Candidate subsets: I={(0,0,0),(0,1,0)}; L={(0,0,0),(1,0,0)}; D={(0,0,0),(1,0,0),(0,0,1),(1,0,1)}, that is all (a,0,c). - U — the ring of 2-by-2 upper-triangular matrices over 𝔽₂, 8 elements - (a,b,c) — the matrix with first row (a,b) and second row (0,c), a,b,c∈{0,1} - E_{11},E_{12},E_{22} — (1,0,0), (0,1,0), (0,0,1) - 1_U=(1,0,1) — the multiplicative identity of U - I,\ L,\ D — the three candidate subsets - \beta\in\{0,1\} — the parameter of an element of I or L ## Rules and sources - 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. - 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. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - 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. - set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x). - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v). - add_zero · prerequisite — Additive identity: u+0=u. - contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q. - forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds. - mul_one · prerequisite — Multiplicative identity: 1·u=u. - subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B). - mko_ideal_def · cited — Given a finite unital ring R and a fully specified subset I, require I to be nonempty and closed under addition and additive inverses, and for every r in R and x in I require both rx and xr to belong to I. Qualification always refers to the same parent ring; left and right absorption are quantified separately. · mko-finite-two-sided-ideal - f2_arith · prerequisite — 𝔽₂={0,1} with arithmetic mod 2: 0+0=0, 0+1=1, 1+1=0; −0=0 and −1=1; 0·t=0 and 1·1=1. - one_sided_subring_def · prerequisite — Left ideal: nonempty, closed under addition and additive inverses, with rx∈J for all r∈R and x∈J (a right ideal symmetrically requires xr∈J). Subring: a subset containing 1 and closed under addition, additive inverses and multiplication. - L_one_in_ideal · lemma — In a unital ring R, if a subset J satisfying right absorption (xr∈J) contains 1, then J=R. ## Main derivation S01 · definitionBefore I\ \text{two-sided ideal of}\ U After I\subseteq U,\ I\neq\varnothing,\ I+I\subseteq I,\ -I\subseteq I,\ \forall r\,\forall x:\ rx\in I,\ \forall r\,\forall x:\ xr\in I Conditions: none Rule: mko_ideal_def · Uses: mko_ideal_def, G2 Leaf basis: mko_ideal_def + def_unfold Unfold the MKO's six obligations for a two-sided ideal: a subset of the parent ring U, nonempty, closed under addition, closed under additive inverses, left absorption and right absorption. Each absorption condition quantifies over all r∈U and x∈I and must be checked separately. The parent ring is fixed as the U of G2. S02 · equivalentBefore I=\{(0,0,0),(0,1,0)\} After I=\{(0,\beta,0):\beta\in\{0,1\}\}\subseteq U,\ \ (0,0,0)\in I Conditions: none Rule: set_builder · Uses: G1, G3, S01 Leaf basis: set_builder + set_extensionality The two elements of I are distinct carrier elements, both triples in {0,1}³, so I⊆U; with the parameter β, I is written as {(0,β,0)}, where β=0 gives the zero and β=1 gives E₁₂. The zero is in I, so I is nonempty. S03 · impliesBefore (0,\beta,0)+(0,\beta',0) After (0,\ (\beta+\beta')\bmod 2,\ 0)\in I Conditions: none Rule: f2_arith · Uses: S02, G1, f2_arith Leaf basis: f2_arith + set_builder Addition is entrywise mod 2: the first and third entries are 0+0=0, and the second entry β+β' mod 2 lies in {0,1}, so the sum again has the form (0,β'',0) and lies in I. This covers all 4 ordered sums (0+0=0, 0+E₁₂=E₁₂, E₁₂+0=E₁₂, E₁₂+E₁₂=0). S04 · impliesBefore -(0,\beta,0) After (0,\ (-\beta)\bmod 2,\ 0)=(0,\beta,0)\in I Conditions: none Rule: f2_arith · Uses: S02, f2_arith Leaf basis: f2_arith + add_inverse Additive inverses are taken entrywise: −0=0 and −β mod 2=β (since −1≡1). So every element is its own additive inverse, and the inverse stays in I. Check: (0,β,0)+(0,β,0)=(0,2β mod 2,0)=(0,0,0). S05 · impliesBefore r\cdot x=(a,b,c)(0,\beta,0),\ \ r\in U,\ x\in I After r\cdot x=(0,\ a\beta\bmod 2,\ 0)\in I Conditions: none Rule: matrix_product_def · Uses: G1, S02 Leaf basis: matrix_product_def + mul_zero + f2_arith Left absorption: by the multiplication formula of G1, with r=(a,b,c) and x=(0,β,0) arbitrary, the product is (a·0, aβ+b·0, c·0). Sub-steps S05.1 and S05.2 compute it entry by entry: the first and third entries are 0 and the second is aβ mod 2∈{0,1}. So rx lies in I. The formula covers all 8 choices of r and 2 of x (16 products) at once. S06 · impliesBefore x\cdot r=(0,\beta,0)(a,b,c),\ \ r\in U,\ x\in I After x\cdot r=(0\cdot a,\ 0\cdot b+\beta c,\ 0\cdot c)=(0,\ \beta c\bmod 2,\ 0)\in I Conditions: none Rule: matrix_product_def · Uses: G1, S02 Leaf basis: matrix_product_def + mul_zero + f2_arith Right absorption must be checked separately because U is not commutative. The multiplication formula gives xr=(0·a, 0·b+βc, 0·c): the first and third entries are 0 and the second is βc mod 2∈{0,1}. So xr∈I for all r∈U and x∈I. S07 · impliesBefore \text{S02 to S06} After I=\{0,E_{12}\}\ \text{is a two-sided ideal of}\ U Conditions: none Rule: and_intro_elim · Uses: S01, S02, S03, S04, S05, S06 Leaf basis: and_intro_elim + mko_ideal_def All six obligations are proved: subset and nonempty (S02), closure under addition (S03), under inverses (S04), left absorption (S05) and right absorption (S06). By conjunction introduction and the definition in S01, I is a two-sided ideal of U. S08 · impliesBefore L=\{(\beta,0,0):\beta\in\{0,1\}\},\ \ r=(a,b,c) After r\cdot(\beta,0,0)=(a\beta,\ a\cdot 0+b\cdot 0,\ c\cdot 0)=(a\beta\bmod 2,0,0)\in L Conditions: none Rule: matrix_product_def · Uses: G1, G3, one_sided_subring_def, f2_arith Leaf basis: matrix_product_def + mul_zero + f2_arith + one_sided_subring_def L is nonempty, E₁₁+E₁₁=(0,0,0) and −E₁₁=E₁₁, so the additive conditions hold as for I. Left absorption: for any r=(a,b,c), r(β,0,0)=(aβ,0,0)∈L. So L is a left ideal. S09 · impliesBefore E_{11}\cdot E_{12}=(1,0,0)(0,1,0) After E_{11}E_{12}=(0,\ 1\cdot1+0\cdot0,\ 0)=(0,1,0)\notin L\ \Rightarrow\ L\ \text{not two-sided} Conditions: none Rule: quantifier_negation · Uses: S08, G1 Leaf basis: quantifier_negation + matrix_product_def + numeric_evaluation Take x=E₁₁∈L and r=E₁₂∈U: the right product xr=(1·0, 1·1+0·0, 0·0)=(0,1,0). Every element of L has second entry 0, so (0,1,0)∉L. The universal statement of right absorption has a counterexample, so L is not a two-sided ideal. This illustrates the misconception identified in the MKO: checking only left absorption. S10 · impliesBefore D=\{(a,0,c)\},\ \ (a,0,c)(a',0,c') After (aa',\ a\cdot0+0\cdot c',\ cc')=(aa',0,cc')\in D,\ \ 1_U=(1,0,1)\in D Conditions: none Rule: one_sided_subring_def · Uses: G1, G3, one_sided_subring_def Leaf basis: one_sided_subring_def + matrix_product_def + mul_zero D is a subring: the product of two diagonal elements has second entry a·0+0·c'=0 and stays diagonal; entrywise addition keeps the second entry 0; every element is its own additive inverse; the identity (1,0,1) is in D. The MKO warns that a subring must not be called an ideal; S11 shows D is not one. S11 · impliesBefore 1_U\in D,\ \ E_{12}\notin D After D\ \text{is not an ideal};\ \text{witness}\ E_{12}\cdot E_{22}=(0,1,0)\notin D Conditions: none Rule: L_one_in_ideal · Uses: S10, G1 Leaf basis: contrapositive + matrix_product_def + numeric_evaluation By Lemma L_one_in_ideal, if D satisfied right absorption and contained 1, then D=U; but E₁₂=(0,1,0)∉D, so D fails right absorption. A concrete witness: E₁₂E₂₂=(0·0, 0·0+1·1, 0·1)=(0,1,0)∉D (left absorption fails too, with r=E₁₂ and x=E₂₂). The lemma is proved in sub-steps S11.1 and S11.2. S12 · impliesBefore \{0\},\ U After r0=0r=0\in\{0\};\ \ rx,xr\in U\ \Rightarrow\ \{0\},\ U\ \text{two-sided ideals} Conditions: none Rule: mko_ideal_def · Uses: G1, mko_ideal_def Leaf basis: mko_ideal_def + mul_zero + add_zero Zero ideal: 0+0=0, −0=0, and r·0=0·r=0 for every r (mul_zero entrywise for matrices). The whole ring: multiplication is closed on U, so absorption is automatic. The MKO notes that both are two-sided ideals. S13 · impliesBefore \text{S07},\ \text{S09},\ \text{S11},\ \text{S12} After I\ \text{two-sided};\ L\ \text{left only};\ D\ \text{subring, not ideal};\ \{0\},U\ \text{two-sided} Conditions: none Rule: and_intro_elim · Uses: S07, S08, S09, S10, S11, S12 Leaf basis: and_intro_elim Combine the four tasks: I={0,E₁₂} is a two-sided ideal; L={0,E₁₁} is a left ideal but not two-sided; the diagonal subring D is not an ideal; {0} and U are two-sided ideals. Every decision refers to the same parent ring U. ## Substeps and lemmas S05.1 · equivalentBefore (a\cdot 0,\ \ast,\ c\cdot 0) After (0,\ \ast,\ 0) Conditions: none Rule: mul_zero · Uses: G1, mul_zero Leaf basis: mul_zero In the first entry aa' we have a'=0, and in the third entry cc' we have c'=0; anything times 0 is 0. S05.2 · impliesBefore a\beta+b\cdot 0 After a\beta\bmod 2\in\{0,1\} Conditions: none Rule: f2_arith · Uses: S05.1, f2_arith Leaf basis: f2_arith + mul_zero + add_zero In the second entry ab'+bc' we have b'=β and c'=0, so it is aβ+0=aβ, which mod 2 lies in {0,1}. Hence the product has the form (0,β'',0) and lies in I. S11.1 · impliesBefore 1\in J,\ \ \forall x\in J\ \forall r\in R:\ xr\in J After \forall r\in R:\ r=1\cdot r\in J Conditions: none Rule: forall_elim · Uses: one_sided_subring_def Leaf basis: forall_elim + mul_one Specialize right absorption to x=1: for every r∈R, 1·r∈J; and 1·r=r (identity), so r∈J. S11.2 · impliesBefore R\subseteq J,\ \ J\subseteq R After J=R Conditions: none Rule: set_extensionality · Uses: S11.1, set_extensionality Leaf basis: set_extensionality + subset_def S11.1 gives R⊆J, and J is a subset of R by assumption, so J=R by extensionality. S11.1 and S11.2 together prove Lemma L_one_in_ideal. ## Reverse audits - S13 · sufficient_goal_reduction · S07, S09, S11, S12, and_intro_elim — Goal G is the conjunction of the four decisions; H is proved forwards by S07, S09, S11 and S12, H⇒G by conjunction introduction, and G is never used as a premise. - S12 · premise_audit · mko_ideal_def, mul_zero — That zero times anything is zero follows from the ring axioms; closure of U comes from the parent qualification (G2). - S11.2 · premise_audit · S11.1, set_extensionality — Both inclusions are available, so the sets are equal. - S11.1 · premise_audit · forall_elim, mul_one — It needs 1∈J and the identity property 1·r=r; only one instance of right absorption is used. - S11 · premise_audit · S10, L_one_in_ideal, contrapositive — It uses the contrapositive of the lemma: J≠R and 1∈J ⇒ J fails right absorption; the concrete product is checked by N6. - S10 · premise_audit · one_sided_subring_def, matrix_product_def — A subring requires closure under multiplication of elements of D, not absorption of every r∈U; D is not claimed to be an ideal. - S09 · premise_audit · S08, quantifier_negation — One counterexample suffices (N5); left absorption from S08 still holds, and the two do not conflict. - S08 · premise_audit · one_sided_subring_def, matrix_product_def, f2_arith — This proves only left absorption; the MKO requires right absorption to be quantified separately, see S09. - S07 · sufficient_goal_reduction · S01, S02, S03, S04, S05, S06, and_intro_elim — Goal G: I is a two-sided ideal. Sufficient condition H: the six obligations; H⇒G by S01. Each part of H is proved forwards from G1 to G3; G is never used as a premise. - S06 · premise_audit · G1, matrix_product_def, mul_zero — This is a different product from S05 (the factors are swapped) and cannot be inferred from S05; it is computed independently here (N4). - S05.2 · premise_audit · f2_arith, S05.1 — Only that the second entry lies in {0,1} is needed; I places no other restriction on the second entry. - S05.1 · inverse_equivalence · mul_zero — a·0=0 is an identity, so both sides have the same value. - S05 · premise_audit · G1, S02, matrix_product_def — No values are assigned to a, b, c, β, so this is a universal certificate, not a sample; N3 recomputes the first and third entries at all 4 combinations of (a,c). - S04 · premise_audit · f2_arith — It relies on characteristic-2 arithmetic (N2); in other rings an additive inverse need not be the element itself and must be checked separately. - S03 · premise_audit · f2_arith, S02 — It uses that addition in 𝔽₂ stays in {0,1} (N1 checks 1+1=0); no converse is claimed. - S02 · inverse_equivalence · set_builder, set_extensionality — As β runs over {0,1} it lists exactly the two elements of I, so both descriptions are the same set. - S01 · premise_audit · mko_ideal_def, G2 — It only unfolds the definition; if the parent ring were changed (for example viewing I inside another ring), the conclusion would not carry over. ## Error controls and negative controls Left absorption alone is not enoughOne misconception named by the MKO is to check only left absorption. L={0,E₁₁} satisfies rx∈L for every r, but E₁₁E₁₂=E₁₂∉L. In a non-commutative ring rx and xr are different products and must be checked separately against every element of the parent ring (S05 and S06 treat them separately). Multiplicative closure does not establish an idealAnother misconception is to check only closure under multiplication. D is closed under products of its own elements and contains 1, so it is a subring, but an ideal must absorb every element of the parent ring; E₁₂E₂₂=E₁₂∉D. More generally, an absorbing subset containing 1 is the whole ring (Lemma L_one_in_ideal), so a proper subring containing 1 can never be an ideal. Qualification is bound to one parent ringThe same subset can behave differently in different parent rings: for example, viewed inside the diagonal subring D, which is commutative, L is a two-sided ideal ((a,0,c)(β,0,0)=(aβ,0,0)=(β,0,0)(a,0,c)); in U it is not. So every decision must name its parent ring. - L={0,E₁₁} has rx∈L for every r∈U, so L is a two-sided ideal of U → reject — Right absorption fails: E₁₁E₁₂=(0,1,0)∉L. - The diagonal set D is closed under multiplication and contains 1, so it is an ideal of U → reject — E₁₂E₂₂=(0,1,0)∉D; an ideal containing 1 must be all of U. - Spot checks with r=1_U and r=E₁₁ put rx and xr in I, so I is a two-sided ideal → reject — The conclusion happens to be true, but spot checks are not a proof; the formula certificates of S05 and S06 for all 8 choices of r are needed. - L is a two-sided ideal of D, so it is also a two-sided ideal of U → reject — Qualification is bound to the parent ring; in U, E₁₁E₁₂=E₁₂∉L. ## Result and limitations In the ring U of 2-by-2 upper-triangular matrices over 𝔽₂: I={(0,0,0),(0,1,0)} is nonempty, closed under addition and inverses, and for every r∈U has rx=(0,aβ,0)∈I and xr=(0,βc,0)∈I, so it is a two-sided ideal. L={(0,0,0),(1,0,0)} has left absorption but E₁₁E₁₂=E₁₂∉L, so it is not two-sided. The diagonal subring D contains 1 but D≠U, and E₁₂E₂₂=E₁₂∉D, so it is not an ideal. {0} and U are two-sided ideals. - U's finite-unital-ring qualification is taken from the parent node (G2) and the ring axioms are not rechecked; the multiplication formula is derived from the matrix product, and the complete 8-by-8 table is not printed cell by cell. - The conclusion in the third negative control is itself true; what is rejected is the reasoning that spot checks constitute a proof. ## Verification and source binding 7 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 2b3540b5dbb78a14560841645c8bd368269c59a972c859b94548f2dadb8878eb - original source SHA-256: 2b3540b5dbb78a14560841645c8bd368269c59a972c859b94548f2dadb8878eb - 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-two-sided-ideal-01.json)