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

目標與範圍

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

逐步主鏈

x\in X

2\mid x-x=0

2\mid x-y

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

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

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

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

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

[1],\ [3]

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

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

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

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

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

\pi:X\to X/R

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

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）