等價類：在完整有限關係上先認證、再求類，並以非等價關係作對照

目標與範圍

在 X={0,1,2,3,4,5} 上，R 由 12 個明列的有序對給出。先完整認證 R 是等價關係，再依定義 [a]={x∈X ∣ aRx} 求出全部類；證明 aRb ⇒ [a]=[b]、任兩類相等或不交、各類覆蓋 X，得 K(R)={{0,3},{1,4},{2,5}}。最後以 S=R∪{(0,1),(1,0)} 說明未通過傳遞性的關係不能形成等價類。

只在 MKO 範圍內工作：載體 0 到 5 與完整關係對集合明示，且先完整通過反身、對稱、傳遞（假設 a1）；類使用同一關係與載體，不以圖像分群猜測（假設 a2）。不建立商集節點或商環；不改動 canonical MKO 或英文 edition。

已知條件與符號

• set_builder
• set_extensionality
• subset_def
• division_algorithm
• eq_refl_symm_trans
• finite_counting_basics

• G1 — 載體 X={0,1,2,3,4,5}（MKO 假設 a1）。
• G2 — R 恰為 12 個有序對：(0,0)、(0,3)、(3,0)、(3,3)、(1,1)、(1,4)、(4,1)、(4,4)、(2,2)、(2,5)、(5,2)、(5,5)；這是完整的關係對集合。
• G3 — 定義：R 通過反身、對稱、傳遞的完整核對後，[a]={x∈X ∣ aRx}，K(R) 是所有 [a] 所成的集合（MKO 敘述）。
• G4 — 對照關係：S=R∪{(0,1),(1,0)}，共 14 個有序對。

• X — 載體 {0,1,2,3,4,5}
• aRb — (a,b)∈R
• r(a) — a 除以 3 的餘數
• [a] — a 的等價類 {x∈X ∣ aRx}
• K(R) — 全部等價類所成的集合

規則與來源

• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
• 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)。
• mko_eqclass_def · cited — 給完整有限載體 X 及已認證等價關係 R，[a]={x 屬 X:aRx}。若 aRb 則 [a]=[b]；任兩等價類相等或不交。不得從抽樣關係或未通過等價公理的 relation 形成 canonical classes。 · mko-equivalence-class
• equiv_rel_def · prerequisite — 等價關係：反身（對所有 a，aRa）、對稱（aRb⇒bRa）、傳遞（aRb 且 bRc ⇒ aRc）。
• L_rel_desc · lemma — R={(a,b)∈X×X ∣ r(a)=r(b)}，其中 r(a) 是 a 除以 3 的餘數。
• L_same_class · lemma — 對等價關係 R：aRb ⇒ [a]=[b]。

逐步主鏈

R=\{(0,0),(0,3),(3,0),(3,3),(1,1),(1,4),(4,1),(4,4),(2,2),(2,5),(5,2),(5,5)\}

R=\{(a,b)\in X\times X\mid r(a)=r(b)\}

a\in X

aRa

aRb

bRa

aRb,\ bRc

aRc

[a]=\{x\in X\mid aRx\}

[0]=[3]=\{0,3\},\ [1]=[4]=\{1,4\},\ [2]=[5]=\{2,5\}

aRb

[a]=[b]

x\in[a]\cap[b]

[a]=[b];\ \text{hence}\ [a]=[b]\ \lor\ [a]\cap[b]=\varnothing

a\in[a]\ \text{for every}\ a

K(R)=\{\{0,3\},\{1,4\},\{2,5\}\},\ 2+2+2=6=|X|

S=R\cup\{(0,1),(1,0)\}

(3,0),(0,1)\in S,\ (3,1)\notin S:\ S\ \text{not transitive}

[a]_S=\{x\mid aSx\}

[0]_S=\{0,1,3\},\ [3]_S=\{0,3\},\ [1]_S=\{0,1,4\}

\text{visual grouping}\ \{0,1,2\},\ \{3,4,5\}

\{0,1,2\}\notin K(R)\ \text{since}\ (0,1)\notin R

\text{S04, S05, S07, S08, S10}

K(R)=\{\{0,3\},\{1,4\},\{2,5\}\};\ S\ \text{yields no classes}

局部子步與引理

(a,b)\in R

r(a)=r(b)

(a,b)\in X\times X,\ r(a)=r(b)

(a,b)\in R

aRb,\ x\in[b]

x\in[a]

aRb,\ x\in[a]

x\in[b],\ \text{so}\ [a]=[b]

逐步反向審查

• S12 · sufficient_goal_reduction · S04, S05, S07, S08, S10 — 目標 G：本稿目標的認證、類、性質與對照。足夠條件 H：S04、S05、S07、S08、S10；H⇒G 由合取。H 由 G1 到 G4 正向證成，沒有把 G 當作前提。
• S11 · premise_audit · S01, S05 — 一個不在 R 中的對就足以否定這個猜測的分群。
• S10 · premise_audit · S09, set_builder — 集合可由 S 的列表逐一重算；相交而不相等的兩個集合直接違反「相等或不交」。
• S09 · premise_audit · G4, S01, quantifier_negation — 一個失敗的三元組 (3,0,1) 就足以否定傳遞性。
• S08 · premise_audit · S02, S05, S07 — 覆蓋需要反身性，不交需要 S07；計數只是一致性核對。
• S07 · premise_audit · S03, S04, S06, contrapositive — 論證在「傳遞得 aRb」這一步用到傳遞性；S10 正顯示沒有傳遞性時這一步失敗。
• S06.2 · premise_audit · S03, S04, S06.1, set_extensionality — 這裡需要對稱；兩個包含都需要傳遞。
• S06.1 · premise_audit · S04, subset_def — 只用傳遞性；另一個包含在 S06.2。
• S06 · premise_audit · S03, S04, L_same_class — 引理需要對稱與傳遞；不宣稱反向（反向 [a]=[b] ⇒ aRb 也成立，但本步不需要）。
• S05 · inverse_equivalence · set_builder, G2 — 集合建構式雙向：x∈[a] ⇔ (a,x)∈R，可逐一對照 G2 的列表。
• S04 · premise_audit · S01, eq_refl_symm_trans, equiv_rel_def — 認證依賴 S01 的完整描述；若只核幾個三元組，不能排除 S 那種失敗（S09）。
• S03 · premise_audit · S01, eq_refl_symm_trans — 對全部 12 個對一次成立。
• S02 · premise_audit · S01, eq_refl_symm_trans — 對全部 6 個元素成立，不是抽樣。
• S01.2 · premise_audit · S01.1, finite_counting_basics — 需要 G2 的 12 個對互異（逐一可見）與計數；若漏列一對，計數就會揭露。
• S01.1 · premise_audit · G2, division_algorithm — 12 個對逐一可核；只證一個包含。
• S01 · inverse_equivalence · L_rel_desc, set_extensionality — 兩個包含都在子步證明，所以集合相等雙向成立。

錯誤控制與反例

先認證等價關係，再形成等價類

MKO 指出的誤解：從未認證的 relation 直接分群。S 看起來與 R 只差兩個對，反身與對稱都成立，但傳遞性失敗（S09），所得集合不構成分割（S10）。必須先完整通過三個公理（S02 到 S04），才求類。

不保留相交而不相等的類

MKO 的第二個誤解。對等價關係，S07 證明相交的兩類必相等；若手上有 {0,1,3} 與 {0,3} 這樣相交卻不相等的集合，表示關係不是等價關係或計算有誤，應回頭檢查，而不是兩者都保留。

不以外觀分群

MKO 假設 a2：類使用同一關係，不以圖像分群猜測。數字相鄰的 {0,1,2} 不是類，因為 (0,1)∉R（S11）。

• S 反身且對稱，所以它的「類」分割 X → reject — S 不傳遞；[0]_S={0,1,3} 與 [3]_S={0,3} 相交而不相等（S10）。
• {0,1,3} 與 {0,3} 可以同時保留為等價類 → reject — 等價類相等或不交；兩者相交於 {0,3} 卻不相等。
• {0,1,2} 是一個類，因為它們是連續的數 → reject — (0,1)∉R，所以 1∉[0]（S11）。
• 抽查三元組 (0,3,0) 與 (1,4,1) 都符合傳遞，所以任何這樣的關係都已認證 → reject — S 也通過這兩個三元組，但 (3,0,1) 失敗；認證要對全部可接續的對（S04 以完整描述一次處理 24 個）。

結論與限制

明列的 12 個對恰為「除以 3 餘數相同」的全部對，因此 R 完整通過反身、對稱、傳遞。其類為 [0]=[3]={0,3}、[1]=[4]={1,4}、[2]=[5]={2,5}；aRb ⇒ [a]=[b]，任兩類相等或不交，且覆蓋 X，K(R)={{0,3},{1,4},{2,5}}。S=R∪{(0,1),(1,0)} 反身且對稱但不傳遞（(3,0)、(0,1)∈S，(3,1)∉S），其「類」{0,1,3} 與 {0,3} 相交而不相等，不能作為等價類。

• 商集 X/R 作為獨立節點及有限環的商環（MKO 的下一步）不在本稿範圍；本稿只求出 K(R) 並證明其分割性質。

驗證及來源綁定

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

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

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