# 模2關係在四元素載體上的商集

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-quotient-set/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-quotient-set-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

X/R={ {0,2},{1,3} }，且投影值是整個類。

完整有限載體及模2等價關係；不自動繼承運算。





## 已知條件與符號


- calc


- G1 — X={0,1,2,3}；xRy 當且僅當2整除x-y。


- E,O — 偶數類與奇數類
- \pi — 正規投影





## 規則與來源


- calc · prerequisite — 假設整數整除法則、集合外延相等與函數定義。
- mko_definition · cited — X/R是所有distinct equivalence classes的集合，不是挑選代表元的集合。classes覆蓋X且兩兩互斥；canonical projection把每個元素送到其class。任何商運算仍需另證代表元無關。 · mko-quotient-set





## 逐步主鏈

S01 · implies操作前

x\in X

操作後

2\mid x-x=0

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

任意元素與自身相關，故關係反身。



S02 · implies操作前

2\mid x-y

操作後

2\mid y-x=-(x-y)

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

取負保留整除性，故關係對稱。



S03 · implies操作前

2\mid x-y,\quad2\mid y-z

操作後

2\mid x-z=(x-y)+(y-z)

條件：無

規則：calc · 依賴：G1, S01, S02

葉節點依據：calc

兩個偶數之和仍偶，證傳遞性，與前兩步合成等價關係。



S04 · implies操作前

[x]=\{y\in X:2\mid y-x\}

操作後

[0]=[2]=\{0,2\}

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

逐查0、1、2、3與0及2的差，完整偶數類均為{0,2}。



S05 · implies操作前

[1],\ [3]

操作後

[1]=[3]=\{1,3\}

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

全部奇數類為{1,3}，四個元素的類已全部計算。



S06 · implies操作前

\{[0],[1],[2],[3]\}

操作後

X/R=\{\{0,2\},\{1,3\}\}

條件：無

規則：mko_definition · 依賴：G1, S04, S05

葉節點依據：mko_definition

以元素排序的集合正規化類，再去除重複，得到兩個商元素。



S07 · implies操作前

E=\{0,2\},\quad O=\{1,3\}

操作後

E\cup O=X,\quad E\cap O=\varnothing

條件：無

規則：calc · 依賴：G1, S06

葉節點依據：calc

明列的兩類覆蓋全部四元素且互斥，所以形成partition。



S08 · implies操作前

\pi:X\to X/R

操作後

\pi(0)=E,\ \pi(1)=O,\ \pi(2)=E,\ \pi(3)=O

條件：無

規則：calc · 依賴：G1, S06, S07

葉節點依據：calc

完整投影表把每個元素送到唯一整個類，並命中全部商元素。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S06, S07 — 輸出是E或O，不是數字0或1；未在商集上宣告新運算。
- S07 · premise_audit · G1, S06 — 兩類均非空；同時核覆蓋與互斥，而非只核類數。
- S06 · premise_audit · G1, S04, S05 — 去重的是相同類而非類內互異元素；{0,1}只是代表元集合。
- S05 · premise_audit · G1, S03 — 1與3相關但與0、2不相關，因此沒有漏類。
- S04 · premise_audit · G1, S03 — 不得只留代表0；2也是類中的元素而非另一商元素。
- S03 · premise_audit · G1, S01, S02 — x、y、z均須屬同一載體X。
- S02 · premise_audit · G1 — 反向再取負回到x-y，沒有方向遺失。
- S01 · premise_audit · G1 — 此式對全部四元素成立，不需另選代表元。





## 錯誤控制與反例

投影型別π的codomain是類的集合，不是所選代表元集合。

良定另證要讓f([x])=g(x)合法，須核xRy推出g(x)=g(y)。


- X/R={0,1}。 → reject — 0與1可作代表，但商元素是兩個集合E、O。
- [0]與[2]是兩個不同商元素。 → reject — 兩類逐元素均為{0,2}。
- 任意X上的函數都會下降到商集。 → reject — f(x)=x在0與2上值不同，故不能定義單值f([0])。





## 結論與限制

X/R={ {0,2},{1,3} }，且投影值是整個類。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 4172954596b8f050df418adbfe5f100efbfc44e67fa2aa975c7d69dddbead328
- original source SHA-256: 0b6728555127f07d75805ac6a167e55fce6180e7883cf8748e68bfbb3b5aab46
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-quotient-set-01.json)