Euclidean distance formula: computing, rejecting the negative root and comparing by squares

Goal and scope

In one equal-unit orthonormal Cartesian frame let P=(1,2), Q=(4,6) and R=(6,−1). Find d(P,Q) and explain why the candidate −5 is not a distance; find the exact form of d(P,R) and decide that it is not an integer; compare d(P,Q) with d(P,R) through their squares; finally check that coincident points have distance zero and that the distance does not depend on the order in which the two points are written.

Works inside the MKO's scope: the plane, two points in one orthonormal frame whose axes use the same unit, integer coordinates. It fully proves the lemma that two nonnegative quantities can be compared through their squares; it does not prove the triangle inequality or that d is a metric, does not treat skew or unequally scaled frames (their difference is only described in an error control), and does not build the Lean EuclideanSpace bridge; it does not change the canonical MKO or its English edition.

Givens and symbols

• numeric_evaluation
• power_laws
• square_nonneg
• sqrt_def
• order_basics

• G1 — Frame: all coordinates are taken in one orthonormal Cartesian frame whose two axes use the same length unit (MKO assumption a1).
• G2 — P=(1,2), Q=(4,6), R=(6,−1), with integer coordinates (MKO assumption a2).
• G3 — Someone proposes the candidate value c=−5 for d(P,Q), on the grounds that (−5)²=25.

• d(P,Q) — the Euclidean distance between P and Q
• (p_x,p_y),\ (q_x,q_y) — the coordinates of P and Q in the same frame
• Q-P — the coordinate differences, taken coordinatewise
• \sqrt{a} — the principal (nonnegative) square root of a≥0
• a,b — two nonnegative reals in the lemma

Rules and sources

• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• 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.
• 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.
• 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.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• 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.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• 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.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• 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.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_distance_def · cited — For P=(x1,y1) and Q=(x2,y2) in the same equal-unit orthonormal Cartesian frame, d(P,Q)=√((x2−x1)²+(y2−y1)²)≥0. Its square is the sum under the root; two such distances can be compared by their squares. · mko-distance-formula
• L_sq_order · lemma — For reals a≥0 and b≥0: a<b ⇔ a²<b².

Main derivation

d(P,Q),\ P=(p_x,p_y),\ Q=(q_x,q_y)

d(P,Q)=\sqrt{(q_x-p_x)^2+(q_y-p_y)^2}

(q_x-p_x)^2+(q_y-p_y)^2

(q_x-p_x)^2+(q_y-p_y)^2\ge 0,\ \ d(P,Q)\ge 0

Q-P

(4-1,\ 6-2)=(3,4)

(q_x-p_x)^2+(q_y-p_y)^2

3^2+4^2=9+16=25

d(P,Q)=\sqrt{25}

d(P,Q)=5

c=-5,\ c^2=25

c\neq d(P,Q)

R-P

(6-1,\ -1-2)=(5,-3)

d(P,R)=\sqrt{5^2+(-3)^2}

d(P,R)=\sqrt{34},\ \ d(P,R)^2=34

d(P,Q)^2=25,\ d(P,R)^2=34,\ 25<34

d(P,Q)<d(P,R)

5^2=25<34<36=6^2

5<\sqrt{34}<6,\ \ \sqrt{34}\notin\mathbb{Z}

d(P,P)

\sqrt{0^2+0^2}=\sqrt{0}=0

(p_x-q_x)^2+(p_y-q_y)^2

(q_x-p_x)^2+(q_y-p_y)^2

\text{tasks of the goal}

d(P,Q)=5,\ d(P,R)=\sqrt{34},\ 5<\sqrt{34}<6,\ -5\neq d(P,Q)

Substeps and lemmas

b=5

b\ge 0\ \land\ b^2=25

5\ge 0,\ 5^2=25

\sqrt{25}=5

0\le a<b

a^2<b^2

a\ge 0,\ b\ge 0,\ a^2<b^2

a<b

Reverse audits

• S13 · sufficient_goal_reduction · S05, S06, S09, S10, S11, S12 — Goal G: the conclusions asked for in the task. Sufficient condition H: the conclusions of S05 to S12 hold together; H⇒G uses only conjunction. H is derived forwards from G1 to G3; G is never used as a premise.
• S12 · inverse_equivalence · neg_mul, add_inverse — This is an identity for all reals (N14), so both directions hold.
• S11 · inverse_equivalence · sqrt_def, numeric_evaluation — Each equality writes the same number in another way, so it holds both ways.
• S10 · premise_audit · S08, L_sq_order, sqrt_def, order_basics — All three numbers must be nonnegative to use the lemma; 'no integer lies strictly between 5 and 6' is an order property of the integers. Only the non-integrality of √34 is derived; no decimal expansion is claimed.
• S09.2 · premise_audit · S09.1, order_basics, contradiction, eq_congruence — The argument by contradiction needs trichotomy to cover every case, and needs b≥0 to apply S09.1.
• S09.1 · premise_audit · order_basics, distributive, mul_zero — a≥0 is needed to make b+a>0; if a could be negative, for example a=−6 and b=5, the conclusion a²<b² fails.
• S09 · premise_audit · S02, L_sq_order — The lemma's hypothesis is that both sides are nonnegative (S02); for numbers that may be negative, comparing squares fails (see the error controls).
• S08 · inverse_equivalence · numeric_evaluation, sqrt_def — Backward: if d≥0 and d²=34, the uniqueness in sqrt_def gives d=√34; the arithmetic under the root can be recomputed (N9).
• S07 · inverse_equivalence · numeric_evaluation — Backward: 1+5=6 and 2+(−3)=−1 restore the coordinates of R.
• S06 · premise_audit · S05, sqrt_def, neg_mul — The rejection rests on the sign condition and uniqueness; it is not claimed that −5 is unrelated to d(P,Q): the two differ only by a sign.
• S05.2 · premise_audit · S05.1, sqrt_def — It needs the uniqueness in sqrt_def and both conditions from S05.1; without b≥0, −5 could not be excluded.
• S05.1 · premise_audit · numeric_evaluation, order_basics — Only one candidate is checked; it is not claimed that 5 is the only real with b²=25 (−5 also has it): uniqueness needs b≥0 as well.
• S05 · inverse_equivalence · sqrt_def, eq_replace — √25 and 5 are the same number and replace each other as equals, so the step holds both ways.
• S04 · inverse_equivalence · numeric_evaluation, power_laws — Each equality is an exact integer computation that can be recomputed independently (N3), so it holds both ways.
• S03 · inverse_equivalence · numeric_evaluation — Backward: 1+3=4 and 2+4=6 restore the coordinates of Q; both sides are the same pair of numbers.
• S02 · premise_audit · S01, square_nonneg, order_basics, sqrt_def — It needs only that real squares are nonnegative and the definition of the principal square root; no converse (recovering anything about the coordinates from d≥0) is claimed.
• S01 · premise_audit · G1, mko_distance_def — This step only states the definition and checks the frame condition; it derives no new fact. If the frame did not satisfy G1, none of the later computations would apply.

Error controls and negative controls

A negative root is not a distance

The first misconception the MKO names is taking a negative square root as the distance. The equation b²=25 has two real solutions, 5 and −5, but the distance is the principal square root and must be nonnegative (S02, S06). A candidate distance must pass two checks: its square equals the sum of squares, and it is nonnegative.

Check the frame first

The formula gives Euclidean distance only in a frame with perpendicular axes and a common length unit. If one grid step is 1 cm on the x-axis and 2 cm on the y-axis, the coordinate difference (3,4) is a physical displacement of 3 cm and 8 cm, and the physical distance is √(9+64)=√73 cm, not 5 cm. If the axes meet at 60° with a common length unit, the squared length of 3e₁+4e₂ is 9+16+2·3·4·cos60°=37, again not 25 (this uses the inner product and is not proved here). That is why S01 first checks G1.

Comparing squares needs nonnegative numbers

Lemma L_sq_order requires a, b≥0. For arbitrary reals it fails: −6<5 but (−6)²=36>25. Distances can be compared by squares because S02 guarantees that they are nonnegative.

• Since (−5)²=25, d(P,Q)=−5 is also a correct answer → reject — The distance is the principal square root and must be ≥0; −5<0.
• d(P,Q)=|3|+|4|=7 → reject — That is the Manhattan (L¹) distance, a different metric; the Euclidean distance is √25=5, and 7≠5.
• d(P,R) equals 5.83 exactly → reject — 5.83²=33.9889≠34; the exact value is √34.
• −6<5, so (−6)²<5² → reject — (−6)²=36>25; comparing by squares works only for nonnegative numbers.

Result and limitations

In one equal-unit orthonormal frame, d(P,Q)=5; the candidate −5 has square 25 but is negative, so it is not a distance. d(P,R)=√34, which is not an integer, and 5<√34<6; from 25<34, d(P,Q)<d(P,R). Coincident points have distance 0, and d(Q,P)=d(P,Q).

• This guide does not prove the triangle inequality or that d satisfies all metric axioms; it uses only d≥0, the squared formula and symmetry.
• The length computation for the 60° skew frame in the error controls uses the inner-product formula, which is not proved here and serves only as a contrast.
• The MKO's formal next step (binding EuclideanSpace ℝ (Fin 2)) is not done.

Verification and source binding

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

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

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