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

目標與範圍

在等單位正交座標系中，取中心 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。

逐步主鏈

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

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

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

d(P,O)\ \square\ r

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

r=5

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

A=(5,3)

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

B=(4,1)

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

E=(-2,3)

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

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

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

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

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

P\in C(O,0)

P=O

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

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

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

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

\text{tasks of the goal}

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

局部子步與引理

0\le s<r

s^2<r^2

s=r

s^2=r^2

0\le r<s

r^2<s^2

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

u^2+v^2=0

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

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

u=0\ \land\ v=0

逐步反向審查

• 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、反控制與修訂記錄）