Similarity: deciding labeled triangle similarity at a specified positive scale and finding the area

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 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.
• 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

S(A,B)\ \text{at a specified scale}\ k

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

k=\tfrac{p}{q}=\tfrac{3}{2}

p=3>0,\ q=2>0\ \Rightarrow\ k>0

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

\det((4,0),(0,2))=4\cdot 2-0\cdot 0=8\neq 0:\ A\ \text{nondegenerate}

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

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

|B_iB_j|=k|A_iA_j|

|B_iB_j|^2=k^2|A_iA_j|^2

|B_iB_j|^2=\left(\tfrac{p}{q}\right)^2|A_iA_j|^2

|B_iB_j|^2\,q^2=|A_iA_j|^2\,p^2

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

16,\ 4,\ 20

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

36,\ 9,\ 45

|B_1B_2|^2q^2\ \text{vs}\ |A_1A_2|^2p^2

36\cdot 2^2=144=16\cdot 3^2

\text{pairs }13,\ 23

9\cdot 2^2=36=4\cdot 3^2,\quad 45\cdot 2^2=180=20\cdot 3^2

|B_iB_j|^2=\tfrac{9}{4}|A_iA_j|^2\ (ij=12,13,23)

S_{3/2}(A,B):\ 6=\tfrac32\cdot 4,\ 3=\tfrac32\cdot 2,\ 3\sqrt5=\tfrac32\cdot 2\sqrt5

\det_A=8>0,\ \det_B=-18<0

\text{opposite orientations; scale still}\ k=\tfrac32>0

S_{3/2}(A,B),\ \mathrm{Area}(A)=4

\mathrm{Area}(B)=\left(\tfrac32\right)^2\cdot 4=9

k=2=\tfrac{2}{1}

36\cdot 1^2=36\neq 64=16\cdot 2^2:\ k=2\ \text{rejected as a witness}

k=-\tfrac32=\tfrac{-3}{2}

p=-3\le 0:\ k\ \text{ineligible}

Substeps and lemmas

k>0,\ u\ge 0

ku\ge 0

v=ku

v^2=(ku)^2=k^2u^2

v^2=k^2u^2,\ v\ge 0,\ ku\ge 0

v=ku

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 witness

k=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 scale

Opposite 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)