Equivalence class: certify a complete finite relation first, then form classes, with a non-equivalence as contrast

Goal and scope

On X={0,1,2,3,4,5}, R is given by 12 explicitly listed ordered pairs. First certify completely that R is an equivalence relation, then compute every class from the definition [a]={x∈X ∣ aRx}; prove that aRb ⇒ [a]=[b], that any two classes are equal or disjoint and that the classes cover X, giving K(R)={{0,3},{1,4},{2,5}}. Finally use S=R∪{(0,1),(1,0)} to show that a relation failing transitivity cannot form equivalence classes.

Works inside the MKO's scope: the carrier 0 to 5 and the complete set of relation pairs are explicit and first pass full reflexivity, symmetry and transitivity checks (assumption a1); the classes use that same relation and carrier, not a visual guess at clustering (assumption a2). It does not set up the quotient-set node or quotient rings, and does not change the canonical MKO or its English edition.

Givens and symbols

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

• G1 — The carrier X={0,1,2,3,4,5} (MKO assumption a1).
• G2 — R consists of exactly 12 ordered pairs: (0,0), (0,3), (3,0), (3,3), (1,1), (1,4), (4,1), (4,4), (2,2), (2,5), (5,2), (5,5); this is the complete set of relation pairs.
• G3 — Definition: after R passes complete checks of reflexivity, symmetry and transitivity, [a]={x∈X ∣ aRx}, and K(R) is the set of all [a] (MKO statement).
• G4 — Contrast relation: S=R∪{(0,1),(1,0)}, 14 ordered pairs in all.

• X — the carrier {0,1,2,3,4,5}
• aRb — (a,b)∈R
• r(a) — the remainder of a on division by 3
• [a] — the class {x∈X ∣ aRx} of a
• K(R) — the set of all equivalence classes

Rules and sources

• 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.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• 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.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• 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).
• mko_eqclass_def · cited — Given a complete finite carrier X and a certified equivalence relation R, define [a]={x in X:aRx}. If aRb then [a]=[b]; any two equivalence classes are equal or disjoint. Sampled relations or relations that fail the equivalence axioms must not be used to form canonical classes. · mko-equivalence-class
• equiv_rel_def · prerequisite — Equivalence relation: reflexive (aRa for all a), symmetric (aRb⇒bRa) and transitive (aRb and bRc ⇒ aRc).
• L_rel_desc · lemma — R={(a,b)∈X×X ∣ r(a)=r(b)}, where r(a) is the remainder of a on division by 3.
• L_same_class · lemma — For an equivalence relation R: aRb ⇒ [a]=[b].

Main derivation

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}

Substeps and lemmas

(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]

Reverse audits

• S12 · sufficient_goal_reduction · S04, S05, S07, S08, S10 — Goal G: the certification, classes, properties and contrast stated in the goal. Sufficient condition H: S04, S05, S07, S08 and S10; H⇒G by conjunction. H is proved forwards from G1 to G4; G is never used as a premise.
• S11 · premise_audit · S01, S05 — One pair not in R suffices to refute the guessed grouping.
• S10 · premise_audit · S09, set_builder — The sets can be recomputed from the list of S; two sets that meet without being equal directly violate 'equal or disjoint'.
• S09 · premise_audit · G4, S01, quantifier_negation — One failing triple (3,0,1) suffices to refute transitivity.
• S08 · premise_audit · S02, S05, S07 — Covering needs reflexivity and disjointness needs S07; the count is a consistency check.
• S07 · premise_audit · S03, S04, S06, contrapositive — The argument uses transitivity at 'transitivity gives aRb'; S10 shows exactly this step failing without transitivity.
• S06.2 · premise_audit · S03, S04, S06.1, set_extensionality — Symmetry is needed here, and both inclusions need transitivity.
• S06.1 · premise_audit · S04, subset_def — Only transitivity is used; the other inclusion is S06.2.
• S06 · premise_audit · S03, S04, L_same_class — The lemma needs symmetry and transitivity; the converse ([a]=[b] ⇒ aRb, also true) is not needed or claimed here.
• S05 · inverse_equivalence · set_builder, G2 — Set-builder membership is two-way: x∈[a] ⇔ (a,x)∈R, checkable against the list of G2 one pair at a time.
• S04 · premise_audit · S01, eq_refl_symm_trans, equiv_rel_def — The certification rests on the complete description of S01; checking only a few triples could not rule out a failure like that of S (S09).
• S03 · premise_audit · S01, eq_refl_symm_trans — It holds for all 12 pairs at once.
• S02 · premise_audit · S01, eq_refl_symm_trans — It holds for all 6 elements, not for a sample.
• S01.2 · premise_audit · S01.1, finite_counting_basics — It needs the 12 pairs of G2 to be distinct (visible one by one) and the count; a missing pair would show up in the count.
• S01.1 · premise_audit · G2, division_algorithm — All 12 pairs can be checked one by one; only one inclusion is proved here.
• S01 · inverse_equivalence · L_rel_desc, set_extensionality — Both inclusions are proved in the sub-steps, so the set equality holds both ways.

Error controls and negative controls

Certify equivalence before forming equivalence classes

The MKO's misconception: grouping directly from an uncertified relation. S differs from R by only two pairs and is reflexive and symmetric, yet transitivity fails (S09) and the sets it yields do not form a partition (S10). All three axioms must be passed completely (S02 to S04) before forming classes.

Do not keep classes that meet without being equal

The MKO's second misconception. For an equivalence relation, S07 proves that two classes that meet are equal; holding sets like {0,1,3} and {0,3}, which meet but differ, signals that the relation is not an equivalence or that a computation is wrong, and calls for a recheck rather than keeping both.

Do not group by appearance

MKO assumption a2: classes use the same relation, not a visual guess at clustering. The consecutive numbers {0,1,2} do not form a class, because (0,1)∉R (S11).

• S is reflexive and symmetric, so its 'classes' partition X → reject — S is not transitive; [0]_S={0,1,3} and [3]_S={0,3} meet without being equal (S10).
• {0,1,3} and {0,3} can both be kept as equivalence classes → reject — Equivalence classes are equal or disjoint; these meet in {0,3} but differ.
• {0,1,2} is a class because they are consecutive numbers → reject — (0,1)∉R, so 1∉[0] (S11).
• The sampled triples (0,3,0) and (1,4,1) satisfy transitivity, so any such relation is certified → reject — S also passes these two triples, yet (3,0,1) fails; certification must cover all composable pairs (S04 handles all 24 at once through the complete description).

Result and limitations

The 12 listed pairs are exactly all pairs with equal remainders on division by 3, so R fully passes reflexivity, symmetry and transitivity. Its classes are [0]=[3]={0,3}, [1]=[4]={1,4}, [2]=[5]={2,5}; aRb ⇒ [a]=[b], any two classes are equal or disjoint, and they cover X, so K(R)={{0,3},{1,4},{2,5}}. S=R∪{(0,1),(1,0)} is reflexive and symmetric but not transitive ((3,0), (0,1)∈S, (3,1)∉S), and its 'classes' {0,1,3} and {0,3} meet without being equal, so they cannot be equivalence classes.

• The quotient set X/R as a node of its own and quotient rings of finite rings (the MKO's next step) are outside this guide; it only computes K(R) and proves its partition properties.

Verification and source binding

8 declared checks for this guide; only the listed expressions are covered.

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

Same-source full JSON (formulas, ASTs, controls and revision log)