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.
Main derivation
S01 · definition
Before
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)>rConditions: 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 · implies
Before
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 · equivalent
Before
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 · equivalent
Before
r=5
After
P\in C(O,5)\iff (x-2)^2+(y+1)^2=25;\ \text{inside}\iff <25;\ \text{outside}\iff >25Conditions: 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 · implies
Before
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 · implies
Before
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 · implies
Before
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 · implies
Before
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 · implies
Before
U=(7,-1),\ V=(-3,-1)
After
d(U,V)=\sqrt{10^2+0^2}=10=2rConditions: 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 · equivalent
Before
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 · implies
Before
r=0,\ d(P,O)<0\ ?
After
\text{no point is strictly inside }C(O,0);\ P\neq O\Rightarrow d(P,O)>0Conditions: 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 · implies
Before
B=(4,1),\ r=0
After
d(B,O)^2=8>0=0^2\ \Rightarrow\ B\ \text{outside};\ O\pm(0,0)=O;\ 2r=0Conditions: 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 · implies
Before
\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 · implies
Before
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 · implies
Before
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 · implies
Before
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 · implies
Before
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 · equivalent
Before
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 · equivalent
Before
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.
Error controls and negative controls
A circle is not a disk
The 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 interior
At 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 excluded
The 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.