# Circle: classifying points as inside, on or outside by squared distance, including radius zero

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

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



## Goal and scope

In an equal-unit orthonormal frame take center O=(2,−1) and radius r=5. Decide whether each of A=(5,3), B=(4,1), E=(−2,3) is strictly inside, on, or outside the circle; verify that the four axial points O±(5,0), O±(0,5) lie on C(O,5), and compute from two opposite axial points the diameter length 2r=10. Then change the radius to r=0, prove that C(O,0)={O} and that no point is strictly inside, and classify B.

Inside the MKO's scope: the Euclidean plane, an equal-unit orthonormal frame, integer coordinates, a nonnegative integer radius. It fully proves two lemmas: a nonnegative distance and a nonnegative radius can be compared through their squares, and a sum of two squares is zero exactly when both numbers are zero. It does not treat negative radii (only explaining in an error control and a negative control why they are excluded), the area or circumference of a disk, or intersections with lines, and does not build the Lean Metric.sphere bridge; it does not change the canonical MKO or its English edition.





## Givens and symbols


- numeric_evaluation
- square_nonneg
- sqrt_def
- order_basics
- distributive


- G1 — Frame: an equal-unit orthonormal Cartesian frame; center and point coordinates are integers and the radius is a nonnegative integer (MKO assumptions a1, a2).
- G2 — O=(2,−1), r=5; A=(5,3), B=(4,1), E=(−2,3).
- G3 — Degenerate case: the same center O with radius r=0.


- C(O,r) — the circle (boundary point set) with center O and radius r
- d(P,O) — the Euclidean distance from P to the center
- r — the nonnegative radius
- (x,y) — the coordinates of a general point P
- s,u,v — reals in the lemmas





## Rules and sources


- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- 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.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- 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.
- 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.
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- 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.
- 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.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_circle_def · cited — In the Euclidean plane, C(O,r)={P:d(P,O)=r} for r≥0. For r>0 this is the ordinary circle boundary; for r=0 it is the singleton {O}. Compare distance with r to classify a point as strictly inside, on the boundary, or outside. The diameter length is 2r. · mko-circle
- 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_cmp · lemma — For reals s≥0 and r≥0: s<r ⇔ s²<r², s=r ⇔ s²=r², and s>r ⇔ s²>r².
- L_sum_sq_zero · lemma — For reals u and v: u²+v²=0 ⇔ u=0 and v=0.





## Main derivation

S01 · definitionBefore

C(O,r),\ r\ge 0

After

C(O,r)=\{P\mid d(P,O)=r\};\ \text{inside}:\ d(P,O)<r;\ \text{outside}:\ d(P,O)>r

Conditions: r\ge 0

Rule: mko_circle_def · Uses: G1

Leaf basis: mko_circle_def + set_builder

State the MKO's definition: the circle is the set of points at distance exactly r from the center, that is, the boundary itself; points at distance less than r are strictly inside and points at distance greater than r are outside. Points strictly inside are not members of C(O,r). The radius must satisfy r≥0 (assumption a2).



S02 · impliesBefore

P=(x,y),\ O=(2,-1)

After

d(P,O)\ge 0,\ \ d(P,O)^2=(x-2)^2+(y+1)^2

Conditions: P,O\ \text{in one orthonormal equal-unit frame}

Rule: mko_distance_def · Uses: S01, G1, G2

Leaf basis: mko_distance_def + sqrt_def + add_inverse

By the distance entry (same equal-unit orthonormal frame, G1), d(P,O)=√((x−2)²+(y−(−1))²)≥0, and y−(−1)=y+1. The radicand is nonnegative, so by sqrt_def the square of the root is the radicand: d(P,O)²=(x−2)²+(y+1)².



S03 · equivalentBefore

d(P,O)\ \square\ r

After

d(P,O)\ \square\ r\iff d(P,O)^2\ \square\ r^2\quad(\square\in\{<,=,>\})

Conditions: d(P,O)\ge 0; r\ge 0

Rule: L_sq_cmp · Uses: S01, S02, L_sq_cmp

Leaf basis: L_sq_cmp

d(P,O)≥0 (S02) and r≥0 (S01), so Lemma L_sq_cmp (s=d(P,O)) applies: each of the three comparisons with r is equivalent to the same comparison between the squared distance and r². This is the MKO's remark that for r≥0 the condition d(P,O)=r may be replaced equivalently by squared distance equal to r². The lemma is proved in S03.1 to S03.4.



S04 · equivalentBefore

r=5

After

P\in C(O,5)\iff (x-2)^2+(y+1)^2=25;\ \text{inside}\iff <25;\ \text{outside}\iff >25

Conditions: r=5\ge 0

Rule: eq_replace · Uses: S02, S03, G2

Leaf basis: eq_replace + numeric_evaluation

Substitute r=5, so r²=25. Combining the squared-distance formula of S02 with the equivalences of S03, the three positions are equivalent to (x−2)²+(y+1)² being equal to, less than, or greater than 25. Each point now needs only one integer computation.



S05 · impliesBefore

A=(5,3)

After

(5-2)^2+(3+1)^2=9+16=25\ \Rightarrow\ A\in C(O,5)

Conditions: none

Rule: numeric_evaluation · Uses: S04, G2

Leaf basis: numeric_evaluation + eq_replace

For A: the differences are (3,4) and 3²+4²=9+16=25, equal to r², so by S04 A lies on the circle.



S06 · impliesBefore

B=(4,1)

After

(4-2)^2+(1+1)^2=8<25\ \Rightarrow\ B\ \text{inside},\ B\notin C(O,5)

Conditions: none

Rule: numeric_evaluation · Uses: S04, S01, G2

Leaf basis: numeric_evaluation + order_basics + mko_circle_def

For B: 2²+2²=8<25, so by S04 B is strictly inside. By S01 a strictly inside point is not a member of C(O,5): B lies in the disk but not on the circle. This is the MKO's warning that a circle is not a disk.



S07 · impliesBefore

E=(-2,3)

After

(-2-2)^2+(3+1)^2=16+16=32>25\ \Rightarrow\ E\ \text{outside}

Conditions: none

Rule: numeric_evaluation · Uses: S04, G2

Leaf basis: numeric_evaluation + neg_mul

For E: (−4)²+4²=16+16=32>25, so by S04 E is outside. Note that −2−2=−4 is negative; its square is 16 (neg_mul).



S08 · impliesBefore

O\pm(5,0),\ O\pm(0,5)

After

(7,-1),\ (-3,-1),\ (2,4),\ (2,-6)\in C(O,5)

Conditions: none

Rule: numeric_evaluation · Uses: S04, G2

Leaf basis: numeric_evaluation + neg_mul + mko_circle_def

Construct the four axial points from explicit directions: O+(5,0)=(7,−1), O−(5,0)=(−3,−1), O+(0,5)=(2,4), O−(0,5)=(2,−6). Their differences from O are (5,0), (−5,0), (0,5), (0,−5), each with squared distance 25+0=25, so by S04 all four lie on the circle (assumption a3). This is an exact construction, not a reading of a picture.



S09 · impliesBefore

U=(7,-1),\ V=(-3,-1)

After

d(U,V)=\sqrt{10^2+0^2}=10=2r

Conditions: none

Rule: mko_distance_def · Uses: S08, mko_distance_def, sqrt_def

Leaf basis: mko_distance_def + sqrt_def + numeric_evaluation

U and V are two opposite axial points. U−V=(10,0) and d(U,V)²=100+0=100; since 10≥0 and 10²=100, sqrt_def gives d(U,V)=10=2·5. The midpoint of U and V is ((7+(−3))/2, (−1+(−1))/2)=(2,−1)=O, so UV is a chord through the center, and its length equals the diameter length 2r stated in the MKO.



S10 · equivalentBefore

P\in C(O,0)

After

P=O

Conditions: r=0

Rule: L_sum_sq_zero · Uses: S02, S03, G3, L_sum_sq_zero

Leaf basis: L_sum_sq_zero + cartesian_product_def + eq_congruence

For r=0: by S03 (s=d(P,O), r=0), P∈C(O,0) ⇔ d(P,O)²=0 ⇔ (x−2)²+(y+1)²=0. By Lemma L_sum_sq_zero (u=x−2, v=y+1) this is equivalent to x−2=0 and y+1=0, that is x=2 and y=−1, which is P=O (equality of ordered pairs). So C(O,0)={O}, the degenerate point set containing only the center. The lemma is proved in S10.1 and S10.2.



S11 · impliesBefore

r=0,\ d(P,O)<0\ ?

After

\text{no point is strictly inside }C(O,0);\ P\neq O\Rightarrow d(P,O)>0

Conditions: r=0

Rule: order_basics · Uses: S02, S10, G3

Leaf basis: order_basics + contradiction

At r=0 being strictly inside needs d(P,O)<0, but S02 gives d(P,O)≥0, and by trichotomy both cannot hold. So at r=0 no point is strictly inside; every P≠O has d(P,O)≠0 (S10), and with d≥0 this gives d(P,O)>0, so P is outside. The center O is on the boundary, not inside.



S12 · impliesBefore

B=(4,1),\ r=0

After

d(B,O)^2=8>0=0^2\ \Rightarrow\ B\ \text{outside};\ O\pm(0,0)=O;\ 2r=0

Conditions: r=0

Rule: numeric_evaluation · Uses: S03, S06, S11, G3

Leaf basis: numeric_evaluation + L_sq_cmp

The squared distance from B to O is still 8 (S06), and 8>0=0², so by S03 B is outside C(O,0). At r=0 the four axial representations O±(0,0) are the same point O (assumption a3), and the diameter length is 2·0=0. The same point B is strictly inside for r=5 and outside for r=0: the classification depends on the radius.



S13 · impliesBefore

\text{tasks of the goal}

After

A\ \text{on},\ B\ \text{inside},\ E\ \text{outside};\ C(O,0)=\{O\}

Conditions: none

Rule: and_intro_elim · Uses: S05, S06, S07, S08, S09, S10, S11, S12

Leaf basis: and_intro_elim

Combine: for r=5, A is on the circle, B is strictly inside (not a member of the circle), E is outside, the four axial points are on the circle and the diameter length is 10; for r=0, C(O,0)={O}, no point is strictly inside, and B is outside.







## Substeps and lemmas

S03.1 · impliesBefore

0\le s<r

After

s^2<r^2

Conditions: s\ge 0

Rule: order_basics · Uses: order_basics, distributive

Leaf basis: order_basics + distributive + mul_zero + add_inverse

From 0≤s<r we get r>0, hence r+s>0, and r−s>0. By order_basics (0<r−s and r+s>0 give 0·(r+s)<(r−s)(r+s)), (r−s)(r+s)>0. By distributivity (r−s)(r+s)=r²−s², so r²−s²>0, that is s²<r².



S03.2 · impliesBefore

s=r

After

s^2=r^2

Conditions: none

Rule: eq_congruence · Uses: eq_congruence

Leaf basis: eq_congruence

Apply the same operation, squaring, to both sides to get s²=r².



S03.3 · impliesBefore

0\le r<s

After

r^2<s^2

Conditions: r\ge 0

Rule: order_basics · Uses: S03.1

Leaf basis: order_basics + distributive

S03.1 holds for any two nonnegative reals; exchanging the roles of s and r (now r≥0 is the smaller one) gives r²<s².



S03.4 · impliesBefore

s<r\Rightarrow s^2<r^2,\ s=r\Rightarrow s^2=r^2,\ s>r\Rightarrow s^2>r^2

After

s<r\iff s^2<r^2,\ s=r\iff s^2=r^2,\ s>r\iff s^2>r^2

Conditions: s\ge 0; r\ge 0

Rule: case_analysis · Uses: S03.1, S03.2, S03.3

Leaf basis: case_analysis + order_basics + contradiction

By trichotomy exactly one of s<r, s=r, s>r holds, and exactly one of the three comparisons between s² and r² holds. Suppose s²<r²: if s=r, S03.2 gives s²=r²; if s>r, S03.3 gives s²>r²; both conflict with s²<r², so s<r. The other two cases are the same. Three forward implications, together with each side's cases being exclusive and exhaustive, give the three equivalences. S03.1 to S03.4 together prove Lemma L_sq_cmp.



S10.1 · equivalentBefore

u^2+v^2=0

After

u^2=0\ \land\ v^2=0

Conditions: none

Rule: square_nonneg · Uses: square_nonneg, order_basics

Leaf basis: square_nonneg + order_basics + add_inverse

From u²+v²=0 we get u²=−v². Since v²≥0, −v²≤0, so u²≤0; also u²≥0 (square_nonneg), so by trichotomy u²=0, and then v²=0−u²=0. Backward: 0+0=0.



S10.2 · equivalentBefore

u^2=0\ \land\ v^2=0

After

u=0\ \land\ v=0

Conditions: none

Rule: square_nonneg · Uses: S10.1, square_nonneg

Leaf basis: square_nonneg

By the second part of square_nonneg, u²=0 ⇔ u=0, used once for u and once for v. S10.1 and S10.2 together prove Lemma L_sum_sq_zero.







## Reverse audits


- S13 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S10, S11, S12 — Goal G: the classifications 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 · premise_audit · S03, S06, numeric_evaluation — It reuses the squared distance from S06; no new distance computation is needed.
- S11 · premise_audit · S02, S10, order_basics — It uses only nonnegativity of distance and S10; this is MKO assumption a2: at r=0 there is no interior, and the center lies on the boundary.
- S10.2 · inverse_equivalence · square_nonneg — u²=0 ⇔ u=0 is itself two-way.
- S10.1 · inverse_equivalence · square_nonneg, order_basics, add_inverse — The forward direction needs both squares to be nonnegative; if negative terms could cancel (as in 1+(−1)=0) the conclusion would fail. The backward direction is plain addition.
- S10 · inverse_equivalence · S03, L_sum_sq_zero, cartesian_product_def — Backward: for P=O both differences are 0, the sum of squares is 0, and d(O,O)=0=r. Every link is a two-way equivalence.
- S09 · premise_audit · S08, mko_distance_def, sqrt_def — Only this pair of opposite points is checked to be 2r apart; the diameter length 2r itself is the MKO's statement and is not proved here for general chords through the center.
- S08 · premise_audit · S04, numeric_evaluation — Each point is computed once (N6 to N9); it is not claimed that these are the only integer points on the circle: A is on it too.
- S07 · premise_audit · S04, numeric_evaluation, neg_mul — It relies on S04 and exact computation (N4, N5); a negative coordinate difference does not affect the nonnegativity of the sum of squares.
- S06 · premise_audit · S04, S01, numeric_evaluation, order_basics — 8<25 gives 'strictly inside', and trichotomy then gives d(B,O)≠5, so B∉C(O,5).
- S05 · premise_audit · S04, numeric_evaluation — It relies on the equivalence of S04 and one exact integer computation (N1).
- S04 · inverse_equivalence · S03, eq_replace — Equal quantities are substituted, and the three equivalences come from S03, so the step holds both ways.
- S03.4 · premise_audit · S03.1, S03.2, S03.3, order_basics, case_analysis — It needs the three cases to be exhaustive and exclusive (trichotomy); nonnegativity of s and r is used only in S03.1 and S03.3.
- S03.3 · premise_audit · S03.1 — Exchanging roles needs the smaller number r to be ≥0, which is the hypothesis r≥0.
- S03.2 · premise_audit · eq_congruence — Only the forward direction is claimed; the converse needs nonnegativity ((−5)²=5² but −5≠5) and is handled in S03.4.
- S03.1 · premise_audit · order_basics, distributive, mul_zero — s≥0 is needed to make r+s>0; the converse is not claimed here and is obtained in S03.4 from trichotomy.
- S03 · inverse_equivalence · L_sq_cmp, S02 — Both directions of the lemma are proved in the sub-steps; the hypothesis is that both sides are nonnegative, which is why negative radii are outside this guide.
- S02 · premise_audit · mko_distance_def, sqrt_def, G1 — It needs both points in one equal-unit orthonormal frame; it is not claimed that the coordinates of P can be recovered from the distance.
- S01 · premise_audit · G1, mko_circle_def — This step only states the definition and the three classes; it derives no new fact.





## Error controls and negative controls

A circle is not a diskThe first misconception identified in the MKO is treating a circle as a disk. B has squared distance 8<25, so B is strictly inside, but C(O,5) contains only points at distance exactly 5, so B∉C(O,5) (S06). Being on the circle is an equation, not an inequality.

Radius zero has no interiorAt r=0 being strictly inside requires d(P,O)<0, but distances are nonnegative, so no point is inside; the center O satisfies d(O,O)=0=r and is the only point on the boundary (S10, S11). Calling the center an inside point at r=0 is a misconception the MKO lists.

Why negative radii are excludedThe squared equivalence of S03 needs r≥0. If r=−5 were forced in, (−5)²=25 equals the square for r=5, and the squared test would wrongly put A on C(O,−5); but d(A,O)=5≠−5, and since distances are nonnegative, {P: d(P,O)=−5} is empty. The MKO puts negative radii outside this pulse's domain, and this guide does not treat them.


- B=(4,1) is inside, so B belongs to the circle C(O,5) → reject — C(O,5) is the boundary; d(B,O)²=8≠25, so B∉C(O,5).
- Since (−5)²=25, C(O,−5) and C(O,5) are the same circle → reject — Negative radii are outside the domain; read literally, d(P,O)=−5 has no solution because distances are nonnegative, whereas A∈C(O,5).
- At r=0 the center O is strictly inside the circle → reject — d(O,O)=0 is not less than 0; O is on the boundary (C(O,0)={O}).
- The diameter length of C(O,5) is 5 → reject — 5 is the radius; the opposite axial points (7,−1) and (−3,−1) are 10=2r apart.





## Result and limitations

For O=(2,−1) and r=5: A is on the circle, B is strictly inside (not a member of the circle), and E is outside; the four axial points (7,−1), (−3,−1), (2,4), (2,−6) are on the circle, and two opposite ones are 10=2r apart. For r=0: C(O,0)={O}, no point is strictly inside, B is outside, and the diameter length is 0.


- Only one pair of opposite axial points is checked to be 2r apart; the proof that every chord through the center has length 2r is not in this guide.
- This guide does not claim to list all integer points of C(O,5) (for example (−1,3) is also on it).
- The MKO's formal next step (binding Metric.sphere and ball, separating positive and zero radius) is not done.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 5b1c2150da0d22273b514a561fc6cc50da5d94f4fd7066a76a31e998bb2070bc
- original source SHA-256: 5b1c2150da0d22273b514a561fc6cc50da5d94f4fd7066a76a31e998bb2070bc
- 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-circle-01.json)