# Similarity: deciding labeled triangle similarity at a specified positive scale and finding the area [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-similarity/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-similarity-01 · production-20261019-adopted-96 ## Goal and scope In one equal-unit orthonormal plane, let A1=(0,0), A2=(4,0), A3=(0,2) and B1=(1,1), B2=(1,7), B3=(4,1), with correspondence Ai↔Bi and scale direction |BiBj|=k|AiAj|, at the specified k=3/2. Decide that they are similar at k=3/2, and from the given area Area(A)=4 find Area(B); then explain why k=2 is rejected only as a witness, why k=−3/2 is not eligible, and why opposite orientation does not change the positive scale. Works only inside the MKO's SSS similarity slice: explicit correspondence, explicit scale direction, k=p/q with q>0, integer coordinates, exact comparison by cross-multiplication. The area uses only the MKO's clause that the area scales by k², starting from the given positive area; no general area theory is developed and no other correspondence is searched. It does not change the canonical MKO or its English edition. ## Givens and symbols - eq_congruence - power_laws - frac_rules - zero_product - order_basics - numeric_evaluation - G1 — Model: one equal-unit orthonormal Euclidean plane ℝ², integer coordinates. - G2 — A1=(0,0), A2=(4,0), A3=(0,2); B1=(1,1), B2=(1,7), B3=(4,1); correspondence Ai↔Bi; scale direction |BiBj|=k|AiAj|. - G3 — Specified scale k=3/2 (p=3, q=2); given Area(A)=4; comparison candidate scales k=2 and k=−3/2. - k=\tfrac{p}{q} — the specified length scale, q>0 - |A_iA_j| — the side length ij of A - S_k(A,B) — similar at scale k under Ai↔Bi - \mathrm{Area}(A) — the given positive area of A - \det(u,v) — the 2×2 determinant with rows u and v ## 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. - power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1. - frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0. - 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 uv holds; u0 give uwvw. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined. - mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0. - 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. - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - 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. - contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q. - mko_sim_slice · cited — For two nondegenerate Euclidean plane triangles with explicit correspondence Ai↔Bi, the SSS similarity slice at a specified positive scale k requires |BiBj|=k|AiAj| for every corresponding side; equivalently, all three squared side lengths scale by k². If a positive area of A is given, the area of B is k² times that value. Reflection does not change the positive length scale. · mko-similarity - 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 rows. · mko-determinant - det_collinear · prerequisite — Three points P, Q, R of the plane are collinear exactly when det(Q−P, R−P)=0; so det≠0 gives three distinct noncollinear points. - L_scale_sq · lemma — For reals k>0, u≥0 and v≥0: v=ku ⇔ v²=k²u². ## Main derivation S01 · definitionBefore S(A,B)\ \text{at a specified scale}\ k After S_k(A,B)\iff k>0\ \land\ A,B\ \text{nondegenerate}\ \land\ |B_iB_j|=k|A_iA_j|\ (ij=12,13,23) Conditions: A_i\leftrightarrow B_i\ \text{explicit}; \text{scale direction explicit} Rule: mko_sim_slice · Uses: G1, G2 Leaf basis: mko_sim_slice Fix the criterion from the MKO: with the correspondence and scale direction explicit, A and B are similar at scale k exactly when k is positive, both are nondegenerate, and all three corresponding sides satisfy |BiBj|=k|AiAj|. The direction matters: here a side of B equals k times a side of A, not the other way round (that scale would be 1/k). S02 · impliesBefore k=\tfrac{p}{q}=\tfrac{3}{2} After p=3>0,\ q=2>0\ \Rightarrow\ k>0 Conditions: q>0 Rule: order_basics · Uses: G3, order_basics Leaf basis: order_basics + mul_inverse_nonzero MKO assumption a2: k=p/q with q>0, and the scale is eligible exactly when p>0. Here p=3>0 and q=2>0. From 2>0 we get 1/2>0 (since 2·(1/2)=1>0; if 1/2≤0, multiplying by the positive 2 would give 1≤0, a contradiction), and multiplying by the positive 3 gives 3/2>0. So k=3/2 is an eligible positive scale. S03 · impliesBefore \det(A_2-A_1,\,A_3-A_1) After \det((4,0),(0,2))=4\cdot 2-0\cdot 0=8\neq 0:\ A\ \text{nondegenerate} Conditions: 8\neq 0 Rule: det_collinear · Uses: G2, det2_def, det_collinear Leaf basis: det2_def + det_collinear + numeric_evaluation A2−A1=(4,0) and A3−A1=(0,2), with determinant 4·2−0·0=8≠0, so A1, A2, A3 are distinct and noncollinear and A is a nondegenerate triangle (MKO assumption a1). S04 · impliesBefore \det(B_2-B_1,\,B_3-B_1) After \det((0,6),(3,0))=0\cdot 0-6\cdot 3=-18\neq 0:\ B\ \text{nondegenerate} Conditions: -18\neq 0 Rule: det_collinear · Uses: G2, det2_def, det_collinear Leaf basis: det2_def + det_collinear + numeric_evaluation B2−B1=(0,6) and B3−B1=(3,0), with determinant 0·0−6·3=−18≠0, so B is also a nondegenerate triangle. The minus sign is read as orientation in S12. S05 · equivalentBefore |B_iB_j|=k|A_iA_j| After |B_iB_j|^2=k^2|A_iA_j|^2 Conditions: k>0; |A_iA_j|\ge 0; |B_iB_j|\ge 0 Rule: L_scale_sq · Uses: S02, dist_formula Leaf basis: eq_congruence + power_laws + zero_product + order_basics By Lemma L_scale_sq (u=|AiAj|, v=|BiBj|), when k>0 and lengths are nonnegative, the length relation is equivalent to the squared-length relation. This is the MKO's 'lengths scale by k exactly when squared lengths scale by k²'; the lemma is proved in S05.1 to S05.3. S06 · equivalentBefore |B_iB_j|^2=\left(\tfrac{p}{q}\right)^2|A_iA_j|^2 After |B_iB_j|^2\,q^2=|A_iA_j|^2\,p^2 Conditions: q\neq 0 Rule: frac_rules · Uses: S05, frac_rules Leaf basis: frac_rules + power_laws + mul_inverse_nonzero + eq_congruence (p/q)²=p²/q²; multiplying both sides by q² (q≠0, so q²≠0) gives the integer cross-multiplied form. This is the MKO's exact check B²q²=A²p²: only integer multiplication, no decimals. S07 · equivalentBefore |A_1A_2|^2,\ |A_1A_3|^2,\ |A_2A_3|^2 After 16,\ 4,\ 20 Conditions: none Rule: dist_formula · Uses: G2, dist_formula Leaf basis: dist_formula + numeric_evaluation In the order 12, 13, 23: (4−0)²+(0−0)²=16; (0−0)²+(2−0)²=4; (0−4)²+(2−0)²=16+4=20. S08 · equivalentBefore |B_1B_2|^2,\ |B_1B_3|^2,\ |B_2B_3|^2 After 36,\ 9,\ 45 Conditions: none Rule: dist_formula · Uses: G2, dist_formula Leaf basis: dist_formula + numeric_evaluation Same order: (1−1)²+(7−1)²=36; (4−1)²+(1−1)²=9; (4−1)²+(1−7)²=9+36=45. S09 · impliesBefore |B_1B_2|^2q^2\ \text{vs}\ |A_1A_2|^2p^2 After 36\cdot 2^2=144=16\cdot 3^2 Conditions: none Rule: numeric_evaluation · Uses: S06, S07, S08, G3 Leaf basis: numeric_evaluation + eq_refl_symm_trans Pair 12: the left side is 36·4=144 and the right side 16·9=144, equal, so by S06 |B1B2|²=(3/2)²|A1A2|². S10 · impliesBefore \text{pairs }13,\ 23 After 9\cdot 2^2=36=4\cdot 3^2,\quad 45\cdot 2^2=180=20\cdot 3^2 Conditions: none Rule: numeric_evaluation · Uses: S06, S07, S08, G3 Leaf basis: numeric_evaluation + eq_refl_symm_trans Pair 13: 9·4=36=4·9; pair 23: 45·4=180=20·9. All three pairs pass the cross-multiplication check, and there is no first unequal witness. S11 · impliesBefore |B_iB_j|^2=\tfrac{9}{4}|A_iA_j|^2\ (ij=12,13,23) After S_{3/2}(A,B):\ 6=\tfrac32\cdot 4,\ 3=\tfrac32\cdot 2,\ 3\sqrt5=\tfrac32\cdot 2\sqrt5 Conditions: k=\tfrac32>0; A,B\ \text{nondegenerate} Rule: mko_sim_slice · Uses: S01, S02, S03, S04, S05, S09, S10 Leaf basis: mko_sim_slice + L_scale_sq + and_intro_elim By S09, S10 and S06, all three squared lengths scale by 9/4; by S05 (the ⇐ direction of the lemma, with k=3/2>0), all three lengths scale by 3/2: 6=(3/2)·4, 3=(3/2)·2, √45=3√5=(3/2)·√20=(3/2)·2√5. Together with the eligibility in S02 to S04, every clause of the criterion in S01 holds, so A and B are similar at k=3/2. S12 · impliesBefore \det_A=8>0,\ \det_B=-18<0 After \text{opposite orientations; scale still}\ k=\tfrac32>0 Conditions: none Rule: mko_sim_slice · Uses: S03, S04, S11 Leaf basis: mko_sim_slice + order_basics + numeric_evaluation The determinants have opposite signs, so B has the opposite orientation: B is obtained from A by reflection across y=x, uniform enlargement by 3/2 and translation by (1,1), that is Bi=(1+(3/2)y, 1+(3/2)x) for Ai=(x,y) (N18 and N19 check B2 and B3). The MKO says reflection does not change the positive length scale; the scale is a ratio of nonnegative lengths, so it stays 3/2, not −3/2. S13 · theorem_applicationBefore S_{3/2}(A,B),\ \mathrm{Area}(A)=4 After \mathrm{Area}(B)=\left(\tfrac32\right)^2\cdot 4=9 Conditions: S_{3/2}(A,B); \mathrm{Area}(A)=4>0 Rule: mko_sim_slice · Uses: S11, G3 Leaf basis: mko_sim_slice + power_laws + numeric_evaluation By the MKO's area clause: once similarity at a positive scale k is established and a positive area of A is given, the area of B is k² times it. k²=9/4, so Area(B)=(9/4)·4=9. It is not k·4=6: area is two-dimensional and scales by k². S14 · impliesBefore k=2=\tfrac{2}{1} After 36\cdot 1^2=36\neq 64=16\cdot 2^2:\ k=2\ \text{rejected as a witness} Conditions: none Rule: numeric_evaluation · Uses: S06, S07, S08 Leaf basis: numeric_evaluation + contrapositive Cross-multiply pair 12 with p=2, q=1: 36·1=36 and 16·4=64 differ, so pair 12 is the first unequal witness and k=2 is not a similarity witness. MKO assumption a3: this rejects only the witness k=2, not similarity itself (S11 shows k=3/2 works). In fact, under this correspondence pair 12 pins the scale: if |B1B2|=k'|A1A2| then 6=4k', so k'=3/2. S15 · impliesBefore k=-\tfrac32=\tfrac{-3}{2} After p=-3\le 0:\ k\ \text{ineligible} Conditions: none Rule: mko_sim_slice · Uses: G3, S01, S05 Leaf basis: mko_sim_slice + order_basics + numeric_evaluation MKO assumption a2: eligibility questions allow p≤0 and answer no. Here p=−3≤0, so k=−3/2 is ineligible. Note that (−3/2)²=9/4, so every squared cross-multiplication would pass; the sign must be checked separately. Looking at lengths directly gives the same: |B1B2|=6 while (−3/2)·4=−6, and a length cannot be negative. ## Substeps and lemmas S05.1 · impliesBefore k>0,\ u\ge 0 After ku\ge 0 Conditions: k>0 Rule: order_basics · Uses: order_basics Leaf basis: order_basics + mul_zero + case_analysis If u=0 then ku=0≥0; if u>0, multiplying by the positive k keeps the inequality: ku>k·0=0. So ku≥0. S05.2 · impliesBefore v=ku After v^2=(ku)^2=k^2u^2 Conditions: none Rule: eq_congruence · Uses: eq_congruence, power_laws Leaf basis: eq_congruence + power_laws Square both sides (the same operation applied to equal numbers), then use (ab)²=a²b². This is the ⇒ direction of the lemma. S05.3 · case_splitBefore v^2=k^2u^2,\ v\ge 0,\ ku\ge 0 After v=ku Conditions: v\ge 0; ku\ge 0 Rule: zero_product · Uses: S05.1, zero_product, distributive Leaf basis: zero_product + distributive + case_analysis + order_basics v²−(ku)²=(v−ku)(v+ku)=0 (N17 checks this identity), so by the zero-product property v−ku=0 or v+ku=0. The first gives v=ku. In the second, v=−ku≤0 (as ku≥0 by S05.1) and v≥0, so v=0, hence ku=0, and again v=ku. S05.1 to S05.3 together prove Lemma L_scale_sq. ## Reverse audits - S15 · premise_audit · G3, S01, S05, mko_sim_slice — The ⇐ direction of S05 needs k>0, so a squared check cannot replace the sign check; the step claims no geometric meaning for a negative scale. - S14 · premise_audit · S06, S07, S08, numeric_evaluation — It uses the equivalence of S06 (an unequal squared form gives an unequal length relation); nothing is claimed about any other correspondence. - S13 · premise_audit · S11, G3, mko_sim_slice — It needs the similarity of S11 and the given positive area; the step does not derive any area theory from coordinates. - S12 · premise_audit · S03, S04, S11, mko_sim_slice — Orientation is read only from the signs of the determinants, and the decision in S11 did not use orientation; the map formula is only a cross-check. - S11 · sufficient_goal_reduction · S01, S02, S03, S04, S05, S09, S10 — Goal G: S_{3/2}(A,B). Sufficient condition H: k>0, both nondegenerate, all three sides scaled by k; H⇒G by the criterion S01. H is proved forwards in S02 to S10; G is never used as a premise. - S10 · premise_audit · S06, S07, S08, numeric_evaluation — Exact integer equalities (N10, N11). - S09 · premise_audit · S06, S07, S08, numeric_evaluation — An exact integer equality (N9); only pair 12 is handled. - S08 · inverse_equivalence · dist_formula, numeric_evaluation — The recomputations are N6, N7, N8. - S07 · inverse_equivalence · dist_formula, numeric_evaluation — The recomputations are N3, N4, N5; both sides name the same number. - S06 · inverse_equivalence · frac_rules, mul_inverse_nonzero — Backward, divide both sides by q², which needs q≠0, guaranteed by the MKO's q>0. - S05.3 · premise_audit · S05.1, zero_product, order_basics — The second case uses ku≥0, supplied here by k>0 and u≥0. If k=−3/2 and u>0, then ku<0 and that reasoning cannot be used directly; if u=0 then ku=0. The concrete nondegenerate triangles have positive side lengths and S02 still excludes negative scales. - S05.2 · premise_audit · eq_congruence, power_laws — Only ⇒ is claimed; the converse uses nonnegativity in S05.3. - S05.1 · premise_audit · order_basics, mul_zero — The guide uses k>0 as a sufficient hypothesis and as an eligibility condition for similarity scales. For the arithmetic conclusion ku≥0 alone, k=0 also works when u≥0; if k<0 and u>0 then ku<0. This does not make zero scale eligible in the declared similarity model. - S05 · inverse_equivalence · L_scale_sq, S02 — Both directions are proved in the sub-steps. The sufficient assumptions k>0 and nonnegative lengths give ku≥0, allowing the squared relation to imply the length relation. The arithmetic boundary k=0 can also work but is ineligible under S02; negative k with positive length causes the sign obstruction. - S04 · premise_audit · G2, det2_def, det_collinear — The recomputation is N2; the minus sign does not affect nondegeneracy. - S03 · premise_audit · G2, det2_def, det_collinear — The recomputation is N1; only det≠0 ⇒ noncollinear is used. - S02 · premise_audit · G3, order_basics — Only 'positive times positive is positive' is used; the step does not claim that 3/2 is the only possible scale (see S14). - S01 · premise_audit · G1, G2, mko_sim_slice — This step only states the criterion and derives no new fact; k is a witness to be checked, not guessed from a figure. ## Error controls and negative controls Lengths scale by k, area by k²One misconception the MKO lists is scaling both lengths and area by k, or taking the squared scale for the length scale. Here lengths scale by 3/2 (6=(3/2)·4), squared lengths by 9/4 (36=(9/4)·16), and area by 9/4 (4 becomes 9). Scaling area by k would give 6; scaling squared lengths by k would give 24 instead of 36. A wrong k rejects only that witnessk=2 fails at pair 12 (36≠64), but this only shows that k=2 is not a witness; with k=3/2 all three pairs pass. MKO assumption a3 says explicitly that failure at the specified k rejects only that scale witness, not every possible similarity scale. A negative coordinate coefficient is not a negative length scaleOpposite orientation (determinants of opposite signs) or multiplying coordinates by a negative number never makes the length scale negative. The MKO notes that uniform scaling of coordinates by −2 has positive length scale 2. Here B involves a reflection, yet the scale is 3/2; k=−3/2 is ineligible because p≤0, even though its square equals that of 3/2. - Area(B)=k·Area(A)=(3/2)·4=6 → reject — Area scales by k²: (9/4)·4=9. - Squared lengths also scale by k, so |B1B2|²=(3/2)·16=24 → reject — |B1B2|²=36=(9/4)·16; squared lengths scale by k². - k=2 fails at pair 12, so A and B are not similar → reject — Only the witness k=2 is rejected; k=3/2 passes all three pairs (S11). - With k=−3/2 every squared cross-multiplication passes, so −3/2 is also an eligible scale → reject — p=−3≤0 is ineligible; a squared check cannot tell k from −k, and (−3/2)·4=−6 cannot equal the length 6. ## Result and limitations A and B are nondegenerate (determinants 8 and −18). Under Ai↔Bi the squared sides 16, 4, 20 and 36, 9, 45 all satisfy B²·2²=A²·3², so A and B are similar at k=3/2, with squared lengths scaled by 9/4; from Area(A)=4 we get Area(B)=9. B has the opposite orientation, but the scale is still the positive 3/2. k=2 fails at pair 12, which rejects only that witness; k=−3/2 is ineligible because p≤0. - The area conclusion uses only the MKO's k² area clause, starting from the given Area(A)=4. N20 is an independent numerical cross-check by |det|/2 (18/2=9); that area formula is not proved here and the argument does not depend on it. - det_collinear is a premise of this guide and is not proved here; only the given correspondence is checked. ## Verification and source binding 21 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: a3e5da3d8b98c14fda10b000ea7223cdb705cfc1824ae646dd1becfcce543568 - original source SHA-256: 58669e6075a82ec69759d174d0aa3477b52d7ff3ba2964ddac1c24f126d02aed - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-similarity-01.json)