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

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

d(P,Q)

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

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

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

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

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

3^2+4^2

25

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

d(P,Q)=5

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

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

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

\sqrt{0}=0

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

s=0

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

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

d(P,R)

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

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

5<\sqrt{26}<6

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

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

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

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

Substeps and lemmas

(p-q)^2

(q-p)^2

a^2+b^2=0

a=0\ \land\ b=0

a=0\ \land\ b=0

a^2+b^2=0

0\le a<b

a^2<b^2

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

a<b

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 adding

One 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 value

The 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 value

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