Finite two-sided ideal: checking left and right absorption separately in an upper-triangular matrix ring

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

I\ \text{two-sided ideal of}\ U

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

I=\{(0,0,0),(0,1,0)\}

I=\{(0,\beta,0):\beta\in\{0,1\}\}\subseteq U,\ \ (0,0,0)\in I

(0,\beta,0)+(0,\beta',0)

(0,\ (\beta+\beta')\bmod 2,\ 0)\in I

-(0,\beta,0)

(0,\ (-\beta)\bmod 2,\ 0)=(0,\beta,0)\in I

r\cdot x=(a,b,c)(0,\beta,0),\ \ r\in U,\ x\in I

r\cdot x=(0,\ a\beta\bmod 2,\ 0)\in I

x\cdot r=(0,\beta,0)(a,b,c),\ \ r\in U,\ x\in I

x\cdot r=(0\cdot a,\ 0\cdot b+\beta c,\ 0\cdot c)=(0,\ \beta c\bmod 2,\ 0)\in I

\text{S02 to S06}

I=\{0,E_{12}\}\ \text{is a two-sided ideal of}\ U

L=\{(\beta,0,0):\beta\in\{0,1\}\},\ \ r=(a,b,c)

r\cdot(\beta,0,0)=(a\beta,\ a\cdot 0+b\cdot 0,\ c\cdot 0)=(a\beta\bmod 2,0,0)\in L

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

E_{11}E_{12}=(0,\ 1\cdot1+0\cdot0,\ 0)=(0,1,0)\notin L\ \Rightarrow\ L\ \text{not two-sided}

D=\{(a,0,c)\},\ \ (a,0,c)(a',0,c')

(aa',\ a\cdot0+0\cdot c',\ cc')=(aa',0,cc')\in D,\ \ 1_U=(1,0,1)\in D

1_U\in D,\ \ E_{12}\notin D

D\ \text{is not an ideal};\ \text{witness}\ E_{12}\cdot E_{22}=(0,1,0)\notin D

\{0\},\ U

r0=0r=0\in\{0\};\ \ rx,xr\in U\ \Rightarrow\ \{0\},\ U\ \text{two-sided ideals}

\text{S07},\ \text{S09},\ \text{S11},\ \text{S12}

I\ \text{two-sided};\ L\ \text{left only};\ D\ \text{subring, not ideal};\ \{0\},U\ \text{two-sided}

Substeps and lemmas

(a\cdot 0,\ \ast,\ c\cdot 0)

(0,\ \ast,\ 0)

a\beta+b\cdot 0

a\beta\bmod 2\in\{0,1\}

1\in J,\ \ \forall x\in J\ \forall r\in R:\ xr\in J

\forall r\in R:\ r=1\cdot r\in J

R\subseteq J,\ \ J\subseteq R

J=R

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 enough

One 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 ideal

Another 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 ring

The 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)