# 圓：以距離平方判定點在圓內、圓上或圓外，並處理零半徑

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-circle/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-circle-01 · production-20261019-adopted-96



## 目標與範圍

在等單位正交座標系中，取中心 O=(2,−1)、半徑 r=5。判定 A=(5,3)、B=(4,1)、E=(−2,3) 各在圓內、圓上或圓外；驗證四個軸向點 O±(5,0)、O±(0,5) 都在 C(O,5) 上，並由兩個相對的軸向點算出直徑長 2r=10。再把半徑改為 r=0，證明 C(O,0)={O}、沒有圓內點，並判定 B 的位置。

只在 MKO 範圍內：歐氏平面、等單位正交框架、整數座標、非負整數半徑。完整證明兩個引理：非負距離與非負半徑可用平方比較；兩個平方之和為零當且僅當兩數皆為零。不處理負半徑（只在錯誤控制與反例中說明為何排除）、圓盤的面積或周長、與直線的交點，也不建立 Lean 的 Metric.sphere 橋接；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- numeric_evaluation
- square_nonneg
- sqrt_def
- order_basics
- distributive


- G1 — 框架：等單位正交座標系；中心與點的座標為整數，半徑為非負整數（MKO 假設 a1、a2）。
- G2 — O=(2,−1)、r=5；A=(5,3)、B=(4,1)、E=(−2,3)。
- G3 — 退化情形：同一中心 O，半徑 r=0。


- C(O,r) — 中心 O、半徑 r 的圓（邊界點集）
- d(P,O) — 點 P 到中心的歐氏距離
- r — 非負半徑
- (x,y) — 一般點 P 的座標
- s,u,v — 引理中的實數





## 規則與來源


- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_circle_def · cited — 在歐氏平面固定中心 O 與半徑 r≥0，C(O,r)={P:d(P,O)=r}；r>0 是通常的非退化圓，r=0 是僅含 O 的退化點集。點距中心小於、等於、大於 r 分別判為內、圓上、外；直徑長為 2r。 · mko-circle
- mko_distance_def · cited — 在平面同一等單位正交座標系，P=(px,py)、Q=(qx,qy) 的歐氏距離為 d(P,Q)=√((qx−px)²+(qy−py)²)≥0。距離平方是兩個座標差平方之和；比較兩個距離可比較其非負平方值。 · mko-distance-formula
- L_sq_cmp · lemma — 對實數 s≥0、r≥0：s<r ⇔ s²<r²，s=r ⇔ s²=r²，s>r ⇔ s²>r²。
- L_sum_sq_zero · lemma — 對實數 u、v：u²+v²=0 ⇔ u=0 且 v=0。





## 逐步主鏈

S01 · definition操作前

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

操作後

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

條件：r\ge 0

規則：mko_circle_def · 依賴：G1

葉節點依據：mko_circle_def + set_builder

寫出 MKO 的定義：圓是與中心距離恰為 r 的點的集合，也就是邊界本身；距離小於 r 的點稱為圓內，大於 r 的點稱為圓外。圓內的點不是 C(O,r) 的成員。半徑必須 r≥0（假設 a2）。



S02 · implies操作前

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

操作後

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

條件：P,O\ \text{in one orthonormal equal-unit frame}

規則：mko_distance_def · 依賴：S01, G1, G2

葉節點依據：mko_distance_def + sqrt_def + add_inverse

依距離條目（同一等單位正交框架，G1），d(P,O)=√((x−2)²+(y−(−1))²)≥0，且 y−(−1)=y+1。根號內非負，依 sqrt_def 根號的平方等於根號內的數，所以 d(P,O)²=(x−2)²+(y+1)²。



S03 · equivalent操作前

d(P,O)\ \square\ r

操作後

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

條件：d(P,O)\ge 0; r\ge 0

規則：L_sq_cmp · 依賴：S01, S02, L_sq_cmp

葉節點依據：L_sq_cmp

d(P,O)≥0（S02），r≥0（S01），所以引理 L_sq_cmp（s=d(P,O)）適用：與 r 的三種比較，分別等價於距離平方與 r² 的同一種比較。這就是 MKO 第一段所說「對 r≥0，可把 d(P,O)=r 等價改成距離平方等於 r²」。引理在 S03.1 到 S03.4 證明。



S04 · equivalent操作前

r=5

操作後

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

條件：r=5\ge 0

規則：eq_replace · 依賴：S02, S03, G2

葉節點依據：eq_replace + numeric_evaluation

代入 r=5，r²=25。結合 S02 的距離平方公式與 S03 的等價，三種位置分別等價於 (x−2)²+(y+1)² 等於、小於、大於 25。之後每個點只需算一個整數。



S05 · implies操作前

A=(5,3)

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S04, G2

葉節點依據：numeric_evaluation + eq_replace

對 A：座標差為 (3,4)，3²+4²=9+16=25，等於 r²，依 S04，A 在圓上。



S06 · implies操作前

B=(4,1)

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S04, S01, G2

葉節點依據：numeric_evaluation + order_basics + mko_circle_def

對 B：2²+2²=8<25，依 S04，B 嚴格在圓內。依 S01，圓內的點不是 C(O,5) 的成員：B 在圓盤中，但不在圓上。這正是 MKO 提醒的「圓不是圓盤」。



S07 · implies操作前

E=(-2,3)

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S04, G2

葉節點依據：numeric_evaluation + neg_mul

對 E：(−4)²+4²=16+16=32>25，依 S04，E 在圓外。注意 −2−2=−4 是負數，平方後為 16（neg_mul）。



S08 · implies操作前

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

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S04, G2

葉節點依據：numeric_evaluation + neg_mul + mko_circle_def

以明示方向構造四個軸向點：O+(5,0)=(7,−1)、O−(5,0)=(−3,−1)、O+(0,5)=(2,4)、O−(0,5)=(2,−6)。它們與 O 的座標差分別是 (5,0)、(−5,0)、(0,5)、(0,−5)，距離平方都是 25+0=25，依 S04 全在圓上（假設 a3）。這是精確構造，不靠圖形目測。



S09 · implies操作前

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

操作後

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

條件：無

規則：mko_distance_def · 依賴：S08, mko_distance_def, sqrt_def

葉節點依據：mko_distance_def + sqrt_def + numeric_evaluation

U、V 是兩個相對的軸向點。U−V=(10,0)，d(U,V)²=100+0=100；10≥0 且 10²=100，依 sqrt_def，d(U,V)=10=2·5。U、V 的中點是 ((7+(−3))/2, (−1+(−1))/2)=(2,−1)=O，所以 UV 是通過中心的弦，長度等於 MKO 所說的直徑長 2r。



S10 · equivalent操作前

P\in C(O,0)

操作後

P=O

條件：r=0

規則：L_sum_sq_zero · 依賴：S02, S03, G3, L_sum_sq_zero

葉節點依據：L_sum_sq_zero + cartesian_product_def + eq_congruence

對 r=0：依 S03（s=d(P,O)、r=0），P∈C(O,0) ⇔ d(P,O)²=0 ⇔ (x−2)²+(y+1)²=0。依引理 L_sum_sq_zero（u=x−2、v=y+1），這等價於 x−2=0 且 y+1=0，即 x=2、y=−1，也就是 P=O（有序對相等）。所以 C(O,0)={O}，是只含中心的退化點集。引理在 S10.1、S10.2 證明。



S11 · implies操作前

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

操作後

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

條件：r=0

規則：order_basics · 依賴：S02, S10, G3

葉節點依據：order_basics + contradiction

r=0 時，圓內需要 d(P,O)<0；但 S02 給 d(P,O)≥0，依三分律兩者不能同時成立。所以 r=0 時沒有圓內點；每個 P≠O 都有 d(P,O)≠0（S10），再由 d≥0 得 d(P,O)>0，因此在圓外。中心 O 在圓上，不在圓內。



S12 · implies操作前

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

操作後

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

條件：r=0

規則：numeric_evaluation · 依賴：S03, S06, S11, G3

葉節點依據：numeric_evaluation + L_sq_cmp

B 與 O 的距離平方仍是 8（S06），8>0=0²，依 S03 B 在 C(O,0) 之外。r=0 時四個軸向表示 O±(0,0) 都是同一點 O（假設 a3），直徑長 2·0=0。同一點 B 在 r=5 時是圓內點，在 r=0 時是圓外點：分類依賴半徑。



S13 · implies操作前

\text{tasks of the goal}

操作後

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

條件：無

規則：and_intro_elim · 依賴：S05, S06, S07, S08, S09, S10, S11, S12

葉節點依據：and_intro_elim

合併：r=5 時 A 在圓上、B 在圓內（不屬於圓）、E 在圓外，四個軸向點在圓上，直徑長 10；r=0 時 C(O,0)={O}，沒有圓內點，B 在圓外。







## 局部子步與引理

S03.1 · implies操作前

0\le s<r

操作後

s^2<r^2

條件：s\ge 0

規則：order_basics · 依賴：order_basics, distributive

葉節點依據：order_basics + distributive + mul_zero + add_inverse

由 0≤s<r 得 r>0，故 r+s>0，且 r−s>0。依 order_basics（0<r−s 且 r+s>0 ⇒ 0·(r+s)<(r−s)(r+s)）得 (r−s)(r+s)>0。依分配律 (r−s)(r+s)=r²−s²，所以 r²−s²>0，即 s²<r²。



S03.2 · implies操作前

s=r

操作後

s^2=r^2

條件：無

規則：eq_congruence · 依賴：eq_congruence

葉節點依據：eq_congruence

對等式兩邊做同一個運算「平方」，得 s²=r²。



S03.3 · implies操作前

0\le r<s

操作後

r^2<s^2

條件：r\ge 0

規則：order_basics · 依賴：S03.1

葉節點依據：order_basics + distributive

S03.1 對任意兩個非負實數成立；把 s 與 r 的角色互換（現在 r≥0 是較小者），得 r²<s²。



S03.4 · implies操作前

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

操作後

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

條件：s\ge 0; r\ge 0

規則：case_analysis · 依賴：S03.1, S03.2, S03.3

葉節點依據：case_analysis + order_basics + contradiction

依三分律，s<r、s=r、s>r 恰有一個成立；s²、r² 之間的三種比較也恰有一個成立。設 s²<r²：若 s=r，S03.2 給 s²=r²；若 s>r，S03.3 給 s²>r²；兩者都與 s²<r² 衝突，所以 s<r。另兩種情形同理。三個正向蘊含，加上兩邊的情形各自互斥且窮盡，就得到三個雙向等價。S03.1 到 S03.4 合起來證得引理 L_sq_cmp。



S10.1 · equivalent操作前

u^2+v^2=0

操作後

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

條件：無

規則：square_nonneg · 依賴：square_nonneg, order_basics

葉節點依據：square_nonneg + order_basics + add_inverse

由 u²+v²=0 得 u²=−v²。v²≥0 推出 −v²≤0，所以 u²≤0；又 u²≥0（square_nonneg），依三分律 u²=0，於是 v²=0−u²=0。反向：0+0=0。



S10.2 · equivalent操作前

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

操作後

u=0\ \land\ v=0

條件：無

規則：square_nonneg · 依賴：S10.1, square_nonneg

葉節點依據：square_nonneg

依 square_nonneg 的第二部分 u²=0 ⇔ u=0，對 u、v 各用一次。S10.1 與 S10.2 合起來證得引理 L_sum_sq_zero。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S10, S11, S12 — 目標 G：題目要求的各項判定。足夠條件 H：S05 到 S12 的結論同時成立；H⇒G 只用合取。H 由 G1 到 G3 正向推出，沒有把 G 當作前提。
- S12 · premise_audit · S03, S06, numeric_evaluation — 重用 S06 的距離平方，不需要新的距離計算。
- S11 · premise_audit · S02, S10, order_basics — 只用到距離非負與 S10；這是 MKO 假設 a2「r=0 沒有內部，中心在圓上」。
- S10.2 · inverse_equivalence · square_nonneg — u²=0 ⇔ u=0 本身是雙向的。
- S10.1 · inverse_equivalence · square_nonneg, order_basics, add_inverse — 正向需要兩個平方都非負；若允許負項相消（例如 1+(−1)=0），結論不成立。反向是直接相加。
- S10 · inverse_equivalence · S03, L_sum_sq_zero, cartesian_product_def — 反向：P=O 時座標差都是 0，平方和為 0，d(O,O)=0=r。每一環都是雙向等價。
- S09 · premise_audit · S08, mko_distance_def, sqrt_def — 只核對這一對相對點的距離為 2r；直徑長 2r 本身是 MKO 的陳述，本稿不對一般通過中心的弦證明。
- S08 · premise_audit · S04, numeric_evaluation — 每點各算一次（N6 到 N9）；不宣稱圓上只有這四個整數點，例如 A 也在圓上。
- S07 · premise_audit · S04, numeric_evaluation, neg_mul — 依賴 S04 與精確計算（N4、N5）；負的座標差不影響平方和的非負性。
- S06 · premise_audit · S04, S01, numeric_evaluation, order_basics — 8<25 推出「圓內」，再由三分律推出 d(B,O)≠5，所以 B∉C(O,5)。
- S05 · premise_audit · S04, numeric_evaluation — 依賴 S04 的等價與一次精確整數計算（N1）。
- S04 · inverse_equivalence · S03, eq_replace — 代換的是相等的量，三個等價由 S03 給出，雙向成立。
- S03.4 · premise_audit · S03.1, S03.2, S03.3, order_basics, case_analysis — 需要三種情形窮盡且互斥（三分律）；s、r 非負只在 S03.1、S03.3 用到。
- S03.3 · premise_audit · S03.1 — 互換角色時需要較小的那個數 r≥0，這正是 r≥0 的假設。
- S03.2 · premise_audit · eq_congruence — 只宣稱正向；反向需要非負條件（(−5)²=5² 但 −5≠5），在 S03.4 處理。
- S03.1 · premise_audit · order_basics, distributive, mul_zero — 需要 s≥0 才能保證 r+s>0；此步不宣稱反向，反向在 S03.4 由三分律取得。
- S03 · inverse_equivalence · L_sq_cmp, S02 — 引理兩個方向都在子步證明；前提是兩邊非負，負半徑因此不在本稿範圍。
- S02 · premise_audit · mko_distance_def, sqrt_def, G1 — 需要兩點在同一等單位正交框架；不宣稱由距離可反推出 P 的座標。
- S01 · premise_audit · G1, mko_circle_def — 此步只寫出定義與三種分類，不推出新事實。





## 錯誤控制與反例

圓不是圓盤MKO 的第一個誤解是把圓當圓盤。B 的距離平方 8<25，B 在圓內，但 C(O,5) 只含距離恰為 5 的點，所以 B∉C(O,5)（S06）。判定「在圓上」必須是等式，不是不等式。

零半徑沒有內部r=0 時，圓內要求 d(P,O)<0，但距離非負，所以沒有圓內點；中心 O 滿足 d(O,O)=0=r，是圓上的唯一點（S10、S11）。把中心說成 r=0 的圓內點是 MKO 列出的誤解。

為什麼排除負半徑S03 的平方等價需要 r≥0。若硬把 r=−5 代入，(−5)²=25 與 r=5 的平方相同，平方判定會誤把 A 當作在 C(O,−5) 上；但 d(A,O)=5≠−5，而且距離非負，所以 {P: d(P,O)=−5} 是空集。MKO 把負半徑排除在本輪論域之外，本稿也不處理。


- B=(4,1) 在圓內，所以 B 屬於圓 C(O,5) → reject — C(O,5) 是邊界；d(B,O)²=8≠25，所以 B∉C(O,5)。
- 因為 (−5)²=25，C(O,−5) 與 C(O,5) 是同一個圓 → reject — 負半徑不在論域內；若照字面，d(P,O)=−5 無解，因為距離非負，而 A∈C(O,5)。
- r=0 時中心 O 在圓內 → reject — d(O,O)=0 不小於 0；O 在圓上（C(O,0)={O}）。
- C(O,5) 的直徑長是 5 → reject — 5 是半徑；相對軸向點 (7,−1)、(−3,−1) 的距離是 10=2r。





## 結論與限制

對 O=(2,−1)、r=5：A 在圓上，B 嚴格在圓內（不是圓的成員），E 在圓外；四個軸向點 (7,−1)、(−3,−1)、(2,4)、(2,−6) 在圓上，相對兩點距離 10=2r。對 r=0：C(O,0)={O}，沒有圓內點，B 在圓外，直徑長 0。


- 只核對了一對相對軸向點的距離為 2r；一般通過中心的弦長為 2r 的證明不在本稿。
- 本稿不宣稱列出 C(O,5) 上的全部整數點（例如 (−1,3) 也在圓上）。
- MKO 的 formal next（綁定 Metric.sphere／ball，分開正半徑與零半徑）未做。





## 驗證及來源綁定

17 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 5b1c2150da0d22273b514a561fc6cc50da5d94f4fd7066a76a31e998bb2070bc
- original source SHA-256: 5b1c2150da0d22273b514a561fc6cc50da5d94f4fd7066a76a31e998bb2070bc
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-circle-01.json)