# Euclidean length: computing the distance between two points exactly from coordinates

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-euclidean-length/)

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-euclidean-length-01 · production-20261019-adopted-96



## Goal and scope

In the Euclidean plane represented by ℝ², let P=(1,−2), Q=(4,2), R=(2,3). Compute d(P,Q)=5 exactly; compute d(P,R)=√26 and prove by comparing squares that 5.09<√26<5.1, showing that 5.1 is only an approximation. For general real coordinates, also prove that the distance is defined and nonnegative, that d(Q,P)=d(P,Q), that d(P,P)=0, and that d(P,Q)=0 ⇔ P=Q.

Uses only the MKO's two-dimensional coordinate distance formula (real coordinates, nonnegative principal square root). It proves basic properties of the formula (nonnegativity, symmetry, and its relation to equality of points); it does not prove the triangle inequality, does not treat the link to an abstract metric or to Mathlib's EuclideanSpace, and does not prove that √26 is irrational. It does not change the canonical MKO or its English edition.





## Givens and symbols


- square_nonneg
- sqrt_def
- order_basics
- cartesian_product_def
- numeric_evaluation


- G1 — Model: the Euclidean plane is represented by ℝ², and the coordinates of points are real numbers (MKO assumptions a1, a2).
- G2 — Definition of distance: for P=(x₁,y₁) and Q=(x₂,y₂), d(P,Q)=√((x₂−x₁)²+(y₂−y₁)²), where √ is the nonnegative principal value (MKO assumption a3).
- G3 — P=(1,−2), Q=(4,2), R=(2,3).


- d(P,Q) — the Euclidean distance between P and Q
- x_2-x_1,\ y_2-y_1 — the two coordinate differences
- s — the radicand (x₂−x₁)²+(y₂−y₁)²
- \sqrt{s} — the nonnegative principal square root of s≥0





## Rules and sources


- 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.
- cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- 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).
- neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
- 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.
- 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.
- 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.
- add_zero · prerequisite — Additive identity: u+0=u.
- 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.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- 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.
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_length_def · cited — Independent append-only source erratum (owner-adopted in this local revision; not merged or published): in the Euclidean plane, for P=(x₁,y₁) and Q=(x₂,y₂), their distance is the nonnegative principal square root of the sum of the squared coordinate differences; it is 0 when P=Q. The original Chinese positive-root wording remains in the parent and revision history. · mko-euclidean-length
- L_neg_sq · lemma — For reals p, q: (p−q)²=(q−p)².
- L_sum_sq_zero · lemma — For reals a, b: a²+b²=0 ⇔ a=0 and b=0.
- L_sq_mono · lemma — For reals a≥0 and b≥0: a<b ⇔ a²<b².





## Main derivation

S01 · definitionBefore

d(P,Q)

After

\sqrt{(x_2-x_1)^2+(y_2-y_1)^2}

Conditions: none

Rule: mko_length_def · Uses: G1, G2, mko_length_def

Leaf basis: mko_length_def + def_unfold

By the MKO's definition: take the two coordinate differences, square each, add, and finally take the nonnegative principal square root. The order is 'difference, square, add, root'; the coordinate differences may not be added directly. The definition treats the horizontal and vertical displacements as two perpendicular components.



S02 · impliesBefore

s=(x_2-x_1)^2+(y_2-y_1)^2

After

s\ge 0,\ d(P,Q)=\sqrt{s}\ge 0

Conditions: x_1,y_1,x_2,y_2\in\mathbb{R}

Rule: square_nonneg · Uses: S01, square_nonneg

Leaf basis: square_nonneg + order_basics + sqrt_def

Both squares are ≥0 (squares of reals are nonnegative), and a sum of two nonnegative numbers is ≥0 (order and addition), so the radicand s≥0 and √s is defined; by the definition of the principal root, √s≥0. So for any two points the distance is defined and nonnegative (MKO assumption a3).



S03 · equivalentBefore

x_2-x_1,\ y_2-y_1\ \text{for}\ P,Q

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G3, S01

Leaf basis: numeric_evaluation + add_inverse + neg_mul

P=(1,−2), Q=(4,2): x₂−x₁=4−1=3 and y₂−y₁=2−(−2)=2+2=4. Subtracting a negative number adds its opposite.



S04 · equivalentBefore

3^2+4^2

After

25

Conditions: none

Rule: numeric_evaluation · Uses: S03

Leaf basis: numeric_evaluation + power_laws

Square first, then add: 3²=9, 4²=16, and 9+16=25.



S05 · equivalentBefore

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

After

d(P,Q)=5

Conditions: 25\ge 0

Rule: sqrt_def · Uses: S02, S04, sqrt_def

Leaf basis: sqrt_def + numeric_evaluation + order_basics

By the definition of the principal root, √25 is the unique real b with b≥0 and b²=25. b=5 satisfies 5≥0 and 5²=25, so √25=5. −5 also satisfies (−5)²=25, but −5<0, so it is not the principal value; a distance cannot be −5.



S06 · equivalentBefore

d(Q,P)=\sqrt{(x_1-x_2)^2+(y_1-y_2)^2}

After

\sqrt{(x_2-x_1)^2+(y_2-y_1)^2}=d(P,Q)

Conditions: none

Rule: L_neg_sq · Uses: S01, L_neg_sq

Leaf basis: L_neg_sq + eq_replace

Swapping P and Q changes the sign of each difference: x₁−x₂=−(x₂−x₁). By Lemma L_neg_sq, (x₁−x₂)²=(x₂−x₁)², and likewise for y, so the radicands agree and d(Q,P)=d(P,Q) for all real coordinates. Example: d(Q,P)=√((1−4)²+(−2−2)²)=√(9+16)=5. The lemma is proved in S06.1.



S07 · equivalentBefore

d(P,P)=\sqrt{(x_1-x_1)^2+(y_1-y_1)^2}

After

\sqrt{0}=0

Conditions: none

Rule: sqrt_def · Uses: S01, sqrt_def

Leaf basis: sqrt_def + mul_zero + add_zero + add_inverse

Comparing P with itself, both differences are 0 and the radicand is 0²+0²=0; 0≥0 and 0²=0, so √0=0 and d(P,P)=0.



S08 · equivalentBefore

\sqrt{s}=0\ \ (s\ge 0)

After

s=0

Conditions: s\ge 0

Rule: sqrt_def · Uses: S02, S07, sqrt_def

Leaf basis: sqrt_def + eq_congruence + mul_zero

⇒: by the definition of the principal root, (√s)²=s, so s=0²=0. ⇐: if s=0 then √0=0 (S07). This turns 'distance 0' into 'radicand 0'.



S09 · equivalentBefore

(x_2-x_1)^2+(y_2-y_1)^2=0

After

x_2=x_1\ \land\ y_2=y_1\ \iff\ P=Q

Conditions: none

Rule: L_sum_sq_zero · Uses: S08, L_sum_sq_zero

Leaf basis: L_sum_sq_zero + cartesian_product_def + add_inverse

By Lemma L_sum_sq_zero (a=x₂−x₁, b=y₂−y₁): the sum of squares is 0 ⇔ both differences are 0 ⇔ x₂=x₁ and y₂=y₁; by equality of ordered pairs this is P=Q. With S08: d(P,Q)=0 ⇔ P=Q. The lemma is proved in S09.1 and S09.2.



S10 · equivalentBefore

d(P,R)

After

\sqrt{(2-1)^2+(3-(-2))^2}=\sqrt{26}

Conditions: none

Rule: mko_length_def · Uses: G3, S01

Leaf basis: mko_length_def + numeric_evaluation

R=(2,3): the x-difference is 2−1=1 and the y-difference is 3−(−2)=5; 1²+5²=1+25=26, so d(P,R)=√26. The exact form √26 is kept rather than replaced by a decimal.



S11 · equivalentBefore

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

After

5<\sqrt{26}<6

Conditions: 5\ge 0,\ \sqrt{26}\ge 0,\ 6\ge 0

Rule: L_sq_mono · Uses: S10, L_sq_mono, sqrt_def

Leaf basis: L_sq_mono + sqrt_def + numeric_evaluation

5, √26 and 6 are all ≥0, and (√26)²=26 (definition of the principal root). By Lemma L_sq_mono: 25<26 ⇔ 5<√26, and 26<36 ⇔ √26<6. So √26 lies between 5 and 6. The lemma is proved in S11.1 and S11.2.



S12 · impliesBefore

5.09^2=25.9081<26<26.01=5.1^2

After

5.09<\sqrt{26}<5.1,\ \sqrt{26}\neq 5.1

Conditions: 5.09\ge 0,\ 5.1\ge 0

Rule: L_sq_mono · Uses: S10, L_sq_mono, sqrt_def

Leaf basis: L_sq_mono + sqrt_def + numeric_evaluation + contradiction

Exactly, 5.09²=25.9081<26 and 5.1²=26.01>26, so L_sq_mono gives 5.09<√26<5.1. In particular 5.1²=26.01≠26, so √26≠5.1: a finite decimal such as 5.1 or 5.0990195 printed by a program is only an approximation (5.0990195²<26, N14), while √26 is the exact distance.



S13 · impliesBefore

\text{S02, S05, S06, S07, S09, S12}

After

d(P,Q)=5,\ d(P,R)=\sqrt{26}\in(5.09,\,5.1);\ d\ge 0,\ d(Q,P)=d(P,Q),\ d(P,Q)=0\iff P=Q

Conditions: none

Rule: and_intro_elim · Uses: S02, S05, S06, S07, S09, S12

Leaf basis: and_intro_elim

Putting the steps together: in the example d(P,Q)=5 and d(P,R)=√26, which lies between 5.09 and 5.1; for all real coordinates, the distance is defined and nonnegative, symmetric, and equal to 0 exactly when the two points coincide.







## Substeps and lemmas

S06.1 · equivalentBefore

(p-q)^2

After

(q-p)^2

Conditions: none

Rule: neg_mul · Uses: add_inverse, neg_mul

Leaf basis: neg_mul + add_inverse + distributive

p−q=−(q−p) (additive inverses); by signs and multiplication (−w)(−w)=w·w, so (p−q)²=(−(q−p))²=(q−p)². This proves Lemma L_neg_sq; it is a polynomial identity (N6).



S09.1 · impliesBefore

a^2+b^2=0

After

a=0\ \land\ b=0

Conditions: a,b\in\mathbb{R}

Rule: square_nonneg · Uses: square_nonneg

Leaf basis: square_nonneg + order_basics + eq_congruence

a²≥0 and b²≥0. From a²+b²=0 we get a²=−b²≤0; together with a²≥0, trichotomy gives a²=0, and square_nonneg (u²=0 ⇔ u=0) gives a=0. Likewise b=0.



S09.2 · impliesBefore

a=0\ \land\ b=0

After

a^2+b^2=0

Conditions: none

Rule: mul_zero · Uses: mul_zero

Leaf basis: mul_zero + add_zero

Conversely: 0·0+0·0=0+0=0. S09.1 and S09.2 together prove both directions of Lemma L_sum_sq_zero.



S11.1 · impliesBefore

0\le a<b

After

a^2<b^2

Conditions: a\ge 0

Rule: order_basics · Uses: distributive, order_basics

Leaf basis: distributive + order_basics + neg_mul

b²−a²=(b−a)(b+a) (check by expanding with distributivity, N17). b−a>0; and b>a≥0 gives b>0, so b+a>0. A product of two positive numbers is positive (order and multiplication), so b²−a²>0, that is a²<b².



S11.2 · impliesBefore

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

After

a<b

Conditions: a\ge 0; b\ge 0

Rule: contrapositive · Uses: S11.1, order_basics

Leaf basis: contrapositive + case_analysis + order_basics

By contraposition: if a<b fails, trichotomy gives a=b or b<a. If a=b then a²=b²; if b<a then S11.1 (with roles swapped, 0≤b<a) gives b²<a². In both cases a²<b² fails. So a²<b² implies a<b. S11.1 and S11.2 together prove Lemma L_sq_mono.







## Reverse audits


- S13 · sufficient_goal_reduction · S02, S05, S06, S07, S08, S09, S12 — The goal is the five statements in the goal field. Sufficient condition H: S05 (the example), S12 (the range), S02 (nonnegativity), S06 (symmetry) and S07 to S09 (when the distance is 0) each hold; H gives the goal by conjunction only. Each part of H is proved forwards from the definition and the prerequisites; the goal is never used as a premise.
- S12 · premise_audit · L_sq_mono, sqrt_def, numeric_evaluation, contradiction — If √26=5.1 then (√26)²=5.1², that is 26=26.01, a contradiction; finitely many decimal places give a range, not an equality.
- S11.2 · premise_audit · S11.1, order_basics, contrapositive, case_analysis — The two cases cover every way a<b can fail; applying S11.1 there needs b≥0.
- S11.1 · premise_audit · distributive, order_basics — a≥0 is what guarantees b+a>0; with a=−7 and b=6, b+a<0 and the conclusion fails.
- S11 · inverse_equivalence · L_sq_mono, sqrt_def — The lemma is a biconditional, but only for nonnegative numbers; for example −7<6 while (−7)²=49>36 (N18).
- S10 · inverse_equivalence · mko_length_def, numeric_evaluation — The same kind of computation as S03 to S04, recomputable (N8).
- S09.2 · premise_audit · mul_zero, add_zero — Direct substitution, with no side condition.
- S09.1 · premise_audit · square_nonneg, order_basics — It needs both squares to be nonnegative; with a negative term allowed (as in 1+(−1)=0, N19), a zero sum would not force each term to be 0. So it holds for squares of reals only.
- S09 · inverse_equivalence · L_sum_sq_zero, cartesian_product_def, S08 — The lemma and equality of ordered pairs are both biconditionals, so both directions hold.
- S08 · inverse_equivalence · sqrt_def, S07 — Each direction has its own reason; s≥0 (S02) is needed, otherwise √s is undefined.
- S07 · inverse_equivalence · sqrt_def, mul_zero, add_zero — The only b with b≥0 and b²=0 is b=0, so the step holds both ways.
- S06.1 · inverse_equivalence · neg_mul, add_inverse — It is an identity and holds both ways.
- S06 · inverse_equivalence · L_neg_sq, eq_replace — The radicands agree term by term, so the replacement of equals holds both ways.
- S05 · inverse_equivalence · sqrt_def, numeric_evaluation — Backward: 5²=25 and 5≥0 is exactly the characterization of √25=5; uniqueness is part of the definition.
- S04 · inverse_equivalence · numeric_evaluation — Exact integer arithmetic, independently recomputable (N3).
- S03 · inverse_equivalence · numeric_evaluation, add_inverse — Backward: 1+3=4 and −2+4=2 give back the coordinates of Q.
- S02 · premise_audit · square_nonneg, order_basics, sqrt_def — It needs squares of reals to be nonnegative; if coordinates could be arbitrary complex numbers this would fail, so assumption a2 (real coordinates) cannot be dropped.
- S01 · premise_audit · G2, mko_length_def — This step only states the definition; whether the root is defined is checked in S02.





## Error controls and negative controls

Square before addingOne misconception the MKO names is adding the coordinate differences without squaring them first. For P, Q, 3+4=7, but 7²=49≠25 (N16), so 7 is not d(P,Q); the correct order is to square first, 9+16=25, then take the root, 5. Differences can be negative, and adding them directly can even cancel: differences 1 and −1 add to 0, but the distance is √(1+1)=√2≠0 (N20).

The square root is the nonnegative principal valueThe other misconception the MKO names is ignoring the nonnegative principal value. −5 also satisfies x²=25, but the distance is the principal value √25=5 (S05); writing d=±5 or d=−5 violates MKO assumption a3. S02 proves d≥0 for any two points.

A floating value is not the exact valueThe MKO notes that a program can compute distances with hypot or a square root, but floating-point representations differ from exact real-number arithmetic. A decimal display of √26 is only an approximation: 5.1²=26.01≠26 (N13) and 5.0990195²<26 (N14). The exact answer is √26, and the comparison of squares in S11 to S12 gives a guaranteed range.


- d(P,Q)=3+4=7 → reject — 7²=49≠25; the distance formula squares before adding (N16).
- d(P,Q)=−5, because (−5)²=25 → reject — The principal square root is nonnegative, so √25=5 (S05).
- √26=5.1 → reject — 5.1²=26.01≠26 (N13); 5.1 is only an approximation.
- If the x-difference is 1 and the y-difference is −1, the differences add to 0, so the distance is 0 → reject — The distance is √(1²+(−1)²)=√2≠0; by S09 the distance is 0 only when the two points coincide (N20).





## Result and limitations

d(P,Q)=√(3²+4²)=√25=5; d(P,R)=√(1²+5²)=√26 with 5.09<√26<5.1, so 5.1 is only an approximation. For any real coordinates, d(P,Q) is defined and ≥0, d(Q,P)=d(P,Q), d(P,P)=0, and d(P,Q)=0 ⇔ P=Q.


- This guide does not prove the triangle inequality or the full metric properties of d; the link to Mathlib's EuclideanSpace and dist mentioned by the MKO is not treated here.
- This guide does not prove that √26 is irrational; it only proves that √26 is not 5.1 and gives a range.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 539f8e100b34dcd38a4feb966f262090b32061cef14dde0554cb042ed2f3f5ba
- original source SHA-256: 59692cf052ef581c917f890361bf9fcff19ab54ab5de2bfb61c90c72770ae0f2
- 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-euclidean-length-01.json)