Congruence: deciding congruence of labeled triangles by the SSS slice

Goal and scope

In one equal-unit orthonormal plane, let A1=(0,0), A2=(4,0), A3=(0,3) and B1=(1,1), B2=(1,5), B3=(4,1), with explicit correspondence Ai↔Bi. First verify by determinants that both triples are nondegenerate triangles, then compare squared side lengths exactly in the order 12, 13, 23 to decide G(A,B); explain why B has the opposite orientation and is still congruent; finally find the first unequal witness for the other correspondence A1↔B1, A2↔B3, A3↔B2, and show that a degenerate triple is not eligible.

Works only inside the MKO's SSS slice: one equal-unit orthonormal coordinate plane, integer coordinates, an explicit correspondence, exact comparison of squared lengths. It does not prove the SSS criterion itself, does not treat other criteria such as SAS or ASA, and does not search over unlabeled correspondences; the reflection map serves only as a cross-check. It does not change the canonical MKO or its English edition.

Givens and symbols

• eq_congruence
• distributive
• zero_product
• order_basics
• sqrt_def
• numeric_evaluation

• G1 — Model: one equal-unit orthonormal Euclidean plane ℝ², with points given by integer coordinates.
• G2 — A1=(0,0), A2=(4,0), A3=(0,3); B1=(1,1), B2=(1,5), B3=(4,1); explicit correspondence A1↔B1, A2↔B2, A3↔B3.
• G3 — Comparison data: the other correspondence A1↔B1, A2↔B3, A3↔B2; degenerate candidate triples D=((0,0),(1,1),(2,2)) and D'=((5,5),(6,6),(7,7)).

• A_i,\ B_i — the vertices of the two triangles, i=1,2,3
• A_i\leftrightarrow B_i — the explicit vertex correspondence
• |PQ| — the Euclidean distance between P and Q
• \det(u,v) — the 2×2 determinant ad−bc with rows u=(a,b) and v=(c,d)
• G(A,B) — A and B are congruent under Ai↔Bi

Rules and sources

• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• sqrt_def · prerequisite — Principal square root: for a≥0, √a is the unique real b with b≥0 and b²=a. Negative numbers have no real square root.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• 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.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• mko_sss_slice · cited — In one equal-unit orthonormal Euclidean plane, for nondegenerate triangles A and B with explicit correspondence Ai↔Bi, this pulse uses the SSS congruence slice: all three corresponding side lengths agree. Compare their squares exactly; reflection reverses orientation without defeating congruence. · mko-congruence
• dist_formula · cited — In one equal-unit orthonormal frame, P=(x1,y1) and Q=(x2,y2) have distance d(P,Q)=√((x2−x1)²+(y2−y1)²)≥0; its square is the sum of the squared coordinate differences. · mko-distance-formula
• det2_def · cited — A real 2×2 matrix M=[[a,b],[c,d]] has determinant det(M)=ad−bc. Here the vectors (a,b) and (c,d) are its two rows, written det((a,b),(c,d)). · mko-determinant
• det_collinear · prerequisite — Three points P, Q, R of the plane are collinear (some line contains all three) exactly when det(Q−P, R−P)=0. A triple with a repeated point is collinear, so det≠0 gives three distinct noncollinear points.
• L_sq_eq · lemma — For reals u≥0 and v≥0: u=v ⇔ u²=v².
• L_T_iso · lemma — The map T(x,y)=(y+1, x+1) (reflection across y=x followed by translation by (1,1)) preserves squared distance: |T(P)T(Q)|²=|PQ|² for all points P, Q.

Main derivation

G(A,B)\ \text{for labeled triangles}

G(A,B)\iff A,B\ \text{nondegenerate}\ \land\ |A_iA_j|=|B_iB_j|\ (ij=12,13,23)

\det(A_2-A_1,\,A_3-A_1)

\det((4,0),(0,3))=4\cdot 3-0\cdot 0=12

\det(A_2-A_1,\,A_3-A_1)=12\neq 0

A_1,A_2,A_3\ \text{distinct, noncollinear: }A\ \text{nondegenerate}

\det(B_2-B_1,\,B_3-B_1)

\det((0,4),(3,0))=0\cdot 0-4\cdot 3=-12\neq 0:\ B\ \text{nondegenerate}

|A_iA_j|=|B_iB_j|

|A_iA_j|^2=|B_iB_j|^2

|A_1A_2|^2,\ |A_1A_3|^2,\ |A_2A_3|^2

16,\ 9,\ 25

|B_1B_2|^2,\ |B_1B_3|^2,\ |B_2B_3|^2

16,\ 9,\ 25

(16,9,25)\ \text{vs}\ (16,9,25)

|A_iA_j|^2=|B_iB_j|^2\ (ij=12,13,23)

|A_iA_j|^2=|B_iB_j|^2\ (ij=12,13,23)

|A_1A_2|=|B_1B_2|=4,\ |A_1A_3|=|B_1B_3|=3,\ |A_2A_3|=|B_2B_3|=5

A,B\ \text{nondegenerate},\ |A_iA_j|=|B_iB_j|\ (ij=12,13,23)

G(A,B)\ \text{under}\ A_i\leftrightarrow B_i

\det(A_2-A_1,A_3-A_1)=12>0,\ \det(B_2-B_1,B_3-B_1)=-12<0

\text{opposite orientations; }G(A,B)\ \text{still holds}

T(x,y)=(y+1,\,x+1)

T(A_1)=B_1,\ T(A_2)=B_2,\ T(A_3)=B_3

A_1\leftrightarrow B_1,\ A_2\leftrightarrow B_3,\ A_3\leftrightarrow B_2

|A_1A_2|^2=16\neq 9=|B_1B_3|^2:\ \text{first unequal witness}\ 12

D=((0,0),(1,1),(2,2))

\det((1,1),(2,2))=1\cdot 2-1\cdot 2=0:\ D\ \text{collinear, not eligible}

Substeps and lemmas

u=v

u^2=v^2

u^2=v^2

(u-v)(u+v)=0

(u-v)(u+v)=0,\ u\ge 0,\ v\ge 0

u=v

|T(P)T(Q)|^2,\ P=(x_1,y_1),\ Q=(x_2,y_2)

((y_2+1)-(y_1+1))^2+((x_2+1)-(x_1+1))^2=(x_2-x_1)^2+(y_2-y_1)^2=|PQ|^2

Reverse audits

• S14 · premise_audit · G3, det2_def, det_collinear — It uses det=0 ⇒ collinear; equal side lengths cannot repair eligibility here.
• S13 · premise_audit · S05, S06, S07, contrapositive — It uses the contrapositive of 'equal lengths ⇒ equal squares'; the step does not claim that A and B are congruent under no correspondence.
• S12.1 · inverse_equivalence · dist_formula, add_comm — Each equality is an identity for all reals, so the whole chain holds both ways; no extra condition is placed on P or Q.
• S12 · premise_audit · G2, L_T_iso — The three images can be recomputed coordinatewise; the lemma is proved in S12.1. The step is a consistency check only and does not claim that the SSS decision requires finding such a map.
• S11 · premise_audit · S02, S04, S10, mko_sss_slice — Orientation is read only from the signs of the determinants; the step does not claim that equal orientation is necessary for congruence, and in fact shows that it is not.
• S10 · sufficient_goal_reduction · S01, S03, S04, S09, mko_sss_slice — Goal G: G(A,B). Sufficient condition H: both are nondegenerate and the three corresponding sides are equal; H⇒G by the SSS slice. H is proved forwards from G2 in S03, S04 and S09; G is never used as a premise.
• S09 · premise_audit · S05, S08, sqrt_def — It needs lengths to be nonnegative, which the distance formula guarantees; the explicit lengths are illustration, and the decision itself uses only equal squares.
• S08 · premise_audit · S06, S07, eq_refl_symm_trans — Only the six values of S06 and S07 are needed. If any differ, the first unequal pair encountered in the declared order 12,13,23 is the first witness; later unequal pairs are not first. The alternative correspondence in S13 illustrates this distinction.
• S07 · inverse_equivalence · dist_formula, numeric_evaluation — The recomputations are N6, N7, N8; both sides name the same number.
• S06 · inverse_equivalence · dist_formula, numeric_evaluation — Each value can be recomputed from the formula (N3, N4, N5); both sides name the same number.
• S05.3 · premise_audit · S05.2, zero_product, order_basics — Case 2 uses u, v≥0; without it, u=2 and v=−2 give u²=v² with u≠v.
• S05.2 · inverse_equivalence · distributive, eq_congruence, add_inverse — Subtracting v² and adding v² undo each other, and the expansion is an identity, so the step holds both ways.
• S05.1 · premise_audit · eq_congruence — This sub-step claims only ⇒; the converse needs nonnegativity and is handled in S05.3.
• S05 · inverse_equivalence · L_sq_eq, dist_formula — Both directions of the lemma are proved in the sub-steps, and its hypothesis u, v≥0 comes from distances being nonnegative; if negatives were allowed, equal squares would not give equal numbers (for example 2 and −2).
• S04 · premise_audit · G2, det2_def, det_collinear — The recomputation is N2; the decision uses only det≠0 ⇒ noncollinear, and the minus sign does not affect eligibility.
• S03 · premise_audit · S02, det_collinear — Only the direction det≠0 ⇒ noncollinear is used; no other property of triangles is claimed here.
• S02 · inverse_equivalence · det2_def, numeric_evaluation — Recompute backwards (N1): 12=4·3−0·0 is exactly the determinant with rows (4,0) and (0,3); both expressions name the same number.
• S01 · premise_audit · G1, G2, mko_sss_slice — This step only states the criterion used here and derives no new fact; it is used only inside the MKO's slice (one orthonormal plane, explicit correspondence).

Error controls and negative controls

Opposite orientation is not non-congruence

One misconception the MKO lists is treating the orientation reversal caused by a reflection as non-congruence. Here the determinants are 12 and −12, so the orientations are opposite, but the SSS slice looks only at nondegeneracy and the three corresponding side lengths, which do not depend on orientation (S11); S12 even exhibits a reflection plus translation sending A to B. Orientation only tells whether a reflection is needed; it does not decide congruence.

Eligibility and correspondence before comparison

The MKO also warns against ignoring nondegeneracy and the labeled correspondence, or guessing congruence from a figure. D and D' have equal corresponding sides but are collinear, not triangles (S14), so nondegeneracy must be checked first. On the other hand, the correspondence is given and may not be rearranged at will: under A1↔B1, A2↔B3, A3↔B2 the pair 12 already differs (S13), and this rejects only that correspondence, not the congruence under Ai↔Bi.

Comparing squares needs nonnegativity

Replacing lengths by squared lengths rests on Lemma L_sq_eq, which needs both numbers to be nonnegative. Distances are nonnegative, so it applies; the same reasoning may not be used for quantities that can be negative (2 and −2 have equal squares). Comparing squares also avoids approximation errors from taking roots such as √25: every comparison is an equality of integers.

• det(A) and det(B) have opposite signs, so A and B are not congruent → reject — Opposite signs only mean opposite orientations; the three corresponding squared sides 16, 9, 25 agree, so A and B are congruent (S10, S11).
• The correspondence A1↔B1, A2↔B3, A3↔B2 fails at pair 12, so A and B are not congruent → reject — This rejects only that correspondence; under the explicit correspondence Ai↔Bi, A and B are congruent.
• D and D' both have corresponding squared sides 2, 8, 2, so they are congruent triangles → reject — det((1,1),(2,2))=0, so both are collinear and not nondegenerate triangles; they are outside this entry.
• Two pairs of equal corresponding sides suffice for congruence → reject — P=((0,0),(5,0),(3,4)) and Q=((0,0),(5,0),(4,3)) are both nondegenerate with squared sides 25, 25 in pairs 12 and 13, but pair 23 is 20 versus 10.

Result and limitations

Both triples are nondegenerate triangles (determinants 12 and −12). Under the explicit correspondence Ai↔Bi the corresponding squared sides in the order 12, 13, 23 are 16, 9, 25 for both, so A and B are congruent, with side lengths 4, 3, 5. B has the opposite orientation (it is the image of A under reflection across y=x followed by translation by (1,1)), which does not defeat congruence. For the other correspondence A1↔B1, A2↔B3, A3↔B2 the first unequal witness is pair 12 (16≠9), which rejects only that correspondence; the collinear triples D and D' have equal corresponding sides but are not eligible.

• The SSS slice is taken from the MKO; this guide does not prove it from a definition of congruence as the existence of an isometry. The map of S12 is only a cross-check consistent with the conclusion.
• det_collinear (three points are collinear ⇔ the determinant of the difference vectors is 0) is a premise of this guide and is not proved here.
• This guide checks only the two correspondences given; it does not search the remaining four vertex permutations.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 83caa0f7f586d45c5a409ca376921926f4b747c37d11d7d8431e892c2d0e380c
• original source SHA-256: 727649daf1fc5c011c5f0341aae0d1188360a7ed505f2b639965409a85d8281c
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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