有限雙邊理想：在上三角矩陣環中分開核對左吸收與右吸收

目標與範圍

父環 U 是 𝔽₂ 上 2×2 上三角矩陣環（元素記為 (a,b,c)，代表第一行 (a,b)、第二行 (0,c)），已通過有限含一環資格。（一）證明 I={(0,0,0),(0,1,0)} 是 U 的雙邊理想。（二）證明 L={(0,0,0),(1,0,0)} 滿足左吸收，但不是雙邊理想。（三）證明對角子環 D={(a,0,c)} 含 1 卻不是理想。（四）說明 {0} 與 U 本身是雙邊理想。

在 MKO 的範圍內工作：父環以完整雙表通過有限含一環資格，候選子集由互異載體元素完整列出（假設 a1）；左吸收與右吸收分開量化，並以對全部父環元素成立的公式證書核對，不以抽樣代替（假設 a2）。不處理商環（下一節點），不重新核對父環公理，不改動 canonical MKO 或英文 edition。

已知條件與符號

• matrix_product_def
• mul_zero
• and_intro_elim
• quantifier_negation
• numeric_evaluation

• G1 — U 的載體是 8 個三元組 (a,b,c)∈{0,1}³；加法逐項 mod 2；乘法 (a,b,c)(a',b',c')=(aa', ab'+bc', cc') mod 2（由矩陣乘積得到）。零元 (0,0,0)，單位元 1_U=(1,0,1)。
• G2 — U 已由父節點以完整加法表與乘法表通過有限含一環資格；本稿不重新核對環公理。
• G3 — 候選子集：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)}，即所有 (a,0,c)。

• U — 𝔽₂ 上 2×2 上三角矩陣環，8 個元素
• (a,b,c) — 第一行 (a,b)、第二行 (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) — U 的乘法單位元
• I,\ L,\ D — 三個候選子集
• \beta\in\{0,1\} — I 或 L 中元素的參數

規則與來源

• matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• mko_ideal_def · cited — 給有限含一環 R 與完整子集 I。I 須非空、對加法及加法逆元封閉，並對所有 r∈R、x∈I 同時有 rx∈I 與 xr∈I。資格永遠綁定同一父環；左吸收與右吸收分開量化。 · mko-finite-two-sided-ideal
• f2_arith · prerequisite — 𝔽₂={0,1} 以 mod 2 運算：0+0=0、0+1=1、1+1=0；−0=0、−1=1；0·t=0、1·1=1。
• one_sided_subring_def · prerequisite — 左理想：非空、對加法與加法逆元封閉，且對所有 r∈R、x∈J 有 rx∈J（右理想對稱地要求 xr∈J）。子環：含 1、對加法、加法逆元與乘法封閉的子集。
• L_one_in_ideal · lemma — 在含一環 R 中，若滿足右吸收（xr∈J）的子集 J 含 1，則 J=R。

逐步主鏈

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}

局部子步與引理

(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

逐步反向審查

• S13 · sufficient_goal_reduction · S07, S09, S11, S12, and_intro_elim — 目標 G 是四項判定的合取；H 由 S07、S09、S11、S12 正向證得，H⇒G 由合取引入，沒有把 G 當作前提。
• S12 · premise_audit · mko_ideal_def, mul_zero — 零乘任何元素為零是環公理的推論；U 的封閉性來自父環資格（G2）。
• S11.2 · premise_audit · S11.1, set_extensionality — 兩個方向的包含都已具備，集合相等。
• S11.1 · premise_audit · forall_elim, mul_one — 需要 1∈J 與單位元性質 1·r=r；只用右吸收的一個特例。
• S11 · premise_audit · S10, L_one_in_ideal, contrapositive — 使用引理的逆否：J≠R 且 1∈J ⇒ J 不滿足右吸收；具體乘積由 N6 核對。
• S10 · premise_audit · one_sided_subring_def, matrix_product_def — 子環要求的是對 D 內元素的乘法封閉，不是對全部 r∈U 的吸收；不宣稱 D 是理想。
• S09 · premise_audit · S08, quantifier_negation — 一個反例足以否定（N5）；S08 的左吸收仍然成立，兩者不矛盾。
• S08 · premise_audit · one_sided_subring_def, matrix_product_def, f2_arith — 這只證明了左吸收；MKO 要求右吸收另外量化，見 S09。
• S07 · sufficient_goal_reduction · S01, S02, S03, S04, S05, S06, and_intro_elim — 目標 G：I 是雙邊理想。足夠條件 H：六項責任；H⇒G 由 S01。H 的每一項都由 G1 到 G3 正向證得，沒有把 G 當作前提。
• S06 · premise_audit · G1, matrix_product_def, mul_zero — 與 S05 是不同的乘積（左右因子對調），不能由 S05 推出；這裡獨立計算（N4）。
• S05.2 · premise_audit · f2_arith, S05.1 — 只需第二項落在 {0,1}；I 對第二項沒有其他限制。
• S05.1 · inverse_equivalence · mul_zero — a·0=0 是恆等式，兩邊同值。
• S05 · premise_audit · G1, S02, matrix_product_def — a、b、c、β 沒有被指定數值，所以這是全稱證書，不是抽樣；N3 在全部 4 個 (a,c) 組合上重算第一、三項。
• S04 · premise_audit · f2_arith — 依賴特徵 2 的算術（N2）；在其他環中加法逆元不一定是自己，必須另外核對。
• S03 · premise_audit · f2_arith, S02 — 用到的是 𝔽₂ 加法封閉於 {0,1}（N1 核 1+1=0）；不宣稱反向。
• S02 · inverse_equivalence · set_builder, set_extensionality — β 取遍 {0,1} 恰好列出 I 的兩個元素，兩種寫法是同一集合。
• S01 · premise_audit · mko_ideal_def, G2 — 只展開定義；若換了父環（例如把 I 看成另一個環的子集），結論不能沿用。

錯誤控制與反例

只核左吸收不夠

MKO 指出的誤解之一是只核左吸收。L={0,E₁₁} 對所有 r 滿足 rx∈L，但 E₁₁E₁₂=E₁₂∉L。在非交換環中 rx 與 xr 是不同的乘積，必須分開對全部父環元素核對（S05、S06 分別處理）。

乘法封閉不足以判定理想

另一個誤解是只核乘法封閉。D 對 D 內乘法封閉且含 1，是子環，但理想要求吸收所有父環元素；E₁₂E₂₂=E₁₂∉D。更一般地，含 1 且吸收的子集必是整個環（引理 L_one_in_ideal），所以真子環若含 1 就不可能是理想。

資格綁定同一父環

同一個子集在不同父環中結論可能不同：例如 L 若被看成對角子環 D 的子集，D 交換，L 在 D 中是雙邊理想（(a,0,c)(β,0,0)=(aβ,0,0)=(β,0,0)(a,0,c)）；但在 U 中不是。所以每個判定都必須寫明父環。

• L={0,E₁₁} 對所有 r∈U 有 rx∈L，所以 L 是 U 的雙邊理想 → reject — 右吸收失敗：E₁₁E₁₂=(0,1,0)∉L。
• 對角集合 D 對乘法封閉且含 1，所以是 U 的理想 → reject — E₁₂E₂₂=(0,1,0)∉D；含 1 的理想必為整個 U。
• 抽查 r=1_U 與 r=E₁₁ 時 rx、xr 都在 I 中，所以 I 是雙邊理想 → reject — 結論雖然正確，但抽查不是證明；需要 S05、S06 對全部 8 個 r 的公式證書。
• L 在 D 中是雙邊理想，所以 L 在 U 中也是雙邊理想 → reject — 資格綁定父環；在 U 中 E₁₁E₁₂=E₁₂∉L。

結論與限制

在 𝔽₂ 上 2×2 上三角矩陣環 U 中：I={(0,0,0),(0,1,0)} 非空、對加法與逆元封閉，且對所有 r∈U 有 rx=(0,aβ,0)∈I、xr=(0,βc,0)∈I，所以是雙邊理想。L={(0,0,0),(1,0,0)} 有左吸收，但 E₁₁E₁₂=E₁₂∉L，不是雙邊理想。對角子環 D 含 1 卻 D≠U，E₁₂E₂₂=E₁₂∉D，不是理想。{0} 與 U 是雙邊理想。

• U 的有限含一環資格取自父節點（G2），本稿未重新核對環公理；乘法公式由矩陣乘積導出，8×8 完整表未逐格印出。
• 第三個負向控制的主張結論本身為真，被拒絕的是「抽查即證明」的推理。

驗證及來源綁定

7 個本稿宣告算術檢查；只支持所列算式。

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

同源完整 JSON（含公式、AST、反控制與修訂記錄）