# 連續：分支函數的中心值與可去商的唯一補點

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

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

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



## 目標與範圍

(1) 對 f_V(x)=2x+1（x<1）、f_V(1)=V、f_V(x)=5x−2（x>1），證明 V=3 時 f_V 在 1 連續，V=4 時不連續；(2) 對 g(x)=2x+1（x<1）、g(1)=3、g(x)=5x−1（x>1），證明 g 在 1 不連續；(3) 對 q(x)=(x²−4)/(x−2)（論域 ℝ∖{2}），證明全實數連續延拓在 2 的值必為 4，且 4 確實可行。

只處理 MKO 的兩側仿射分支模型（中心值明示）與可去商的補點延拓，全部以 ε-δ 直接論證，並與 MKO 的「左極限=右極限=V」判準對照。不證明一般的連續性代數或中間值定理。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- abs_rules
- order_basics
- distributive
- frac_rules
- continuity_def
- numeric_evaluation


- G1 — 函數 f:ℝ→ℝ 定義在整個實數上，中心點值明示。
- G2 — f_V(x)=2x+1（x<1），f_V(1)=V，f_V(x)=5x−2（x>1）；比較 V=3 與 V=4。
- G3 — g(x)=2x+1（x<1），g(1)=3，g(x)=5x−1（x>1）。
- G4 — q(x)=(x²−4)/(x−2)，論域 ℝ∖{2}；延拓 F_W(x)=q(x)（x≠2）、F_W(2)=W。


- f_V — 中心值為 V 的兩側仿射分支函數
- L^-,\ L^+ — 左、右極限
- (L^- - V,\ L^+ - V) — 點缺陷對
- q — 可去商，論域 ℝ∖{2}
- F_W — q 的全實數延拓，F_W(2)=W





## 規則與來源


- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- 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。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- continuity_def · prerequisite — 連續（ε-δ）：f 在 a 連續表示對每個 ε>0，存在 δ>0，使所有滿足 |x−a|<δ 的定義域點 x 都有 |f(x)−f(a)|<ε。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- mko_continuity · cited — 對 f:ℝ→ℝ，f 在 a 連續指每個 ε>0 都有 δ>0，使 |x−a|<δ 時 |f(x)−f(a)|<ε；等價地去心兩側極限等於已定義點值 f(a)。兩側仿射、中心明示值 V 的模型，在 a 連續當且僅當左極限=右極限=V。可去商的全 ℝ 連續延拓唯一所需中心值為 2a。 · mko-continuity
- L_branch_bound · lemma — 對所有實數 x：|f_3(x)−3|≤5|x−1|。
- L_unique_ext · lemma — 若 F:ℝ→ℝ 在 x≠2 處 F(x)=x+2，且 F 在 2 連續，則 F(2)=4。





## 逐步主鏈

S01 · definition操作前

f\ \text{continuous at}\ a

操作後

\forall\varepsilon>0\ \exists\delta>0\ \forall x\in\mathbb{R}:\ |x-a|<\delta\Rightarrow|f(x)-f(a)|<\varepsilon

條件：f(a)\ \text{defined}

規則：mko_continuity · 依賴：G1, continuity_def

葉節點依據：continuity_def + def_unfold

依 MKO 展開在 a 的連續性。與去心極限不同，條件 |x−a|<δ 包含 x=a，而且比較對象是已定義的點值 f(a)；所以中心值本身是判定的一部分。



S02 · definition操作前

f_V\ \text{by three cases}

操作後

f_V:\mathbb{R}\to\mathbb{R}\ \text{total},\ f_V(1)=V

條件：無

規則：function_def · 依賴：G2, function_def

葉節點依據：function_def + order_basics

三個情況 x<1、x=1、x>1 互斥且涵蓋全部實數，每個 x 恰得一個值，所以 f_V 是 ℝ 上的函數；中心值 V 是獨立給定的資料，不由分支公式決定。



S03 · equivalent操作前

\text{left branch at }1,\ \text{right branch at }1

操作後

L^-=2\cdot 1+1=3,\ L^+=5\cdot 1-2=3

條件：無

規則：numeric_evaluation · 依賴：G2

葉節點依據：numeric_evaluation

依 MKO 假設 a2，仿射分支的單側極限是分支公式在 a 的值：左 2·1+1=3，右 5·1−2=3（N1、N2）。兩者都與 V 無關。



S04 · theorem_application操作前

L^-=L^+=3

操作後

f_V\ \text{continuous at}\ 1\iff V=3

條件：無

規則：mko_continuity · 依賴：S03, mko_continuity

葉節點依據：mko_continuity

依 MKO 的模型判準：連續當且僅當左極限=右極限=V。左右都是 3，所以條件化為 V=3。等價地，點缺陷對 (3−V, 3−V) 必須是 (0,0)。S05 至 S08 以 ε-δ 直接核對兩個方向的具體情況，不只依賴這個引用的判準。



S05 · implies操作前

V=3

操作後

\forall x\in\mathbb{R}:\ |f_3(x)-3|\le 5|x-1|

條件：無

規則：L_branch_bound · 依賴：G2, S02

葉節點依據：case_analysis + abs_rules + order_basics

依引理 L_branch_bound，三個情況合起來，f_3 與 3 的距離不超過 5|x−1|。引理在 S05.1 至 S05.3 分情況證明。



S06 · implies操作前

\varepsilon>0\ \text{arbitrary},\ \delta=\tfrac{\varepsilon}{5}

操作後

|x-1|<\delta\Rightarrow|f_3(x)-f_3(1)|\le 5|x-1|<\varepsilon;\ f_3\ \text{continuous at}\ 1

條件：\varepsilon>0

規則：forall_intro · 依賴：S01, S05

葉節點依據：forall_intro + exists_intro + order_basics + continuity_def

取任意 ε>0，令 δ=ε/5>0。若 |x−1|<δ，由 S05 與 f_3(1)=3，|f_3(x)−f_3(1)|≤5|x−1|<5δ=ε。ε 任意，依 S01，f_3 在 1 連續，與 S04 的判準一致。例如 ε=1/10 時 δ=1/50（N11）。



S07 · implies操作前

V=4

操作後

(L^- - V,\ L^+ - V)=(-1,-1)\neq(0,0)

條件：無

規則：mko_continuity · 依賴：S03, S04, G2

葉節點依據：mko_continuity + numeric_evaluation

V=4 時點缺陷對為 (3−4, 3−4)=(−1,−1)（N5），不是 (0,0)。左右極限相等（都是 3），卻不等於中心值，依 S04 的判準不連續。S08 以 ε-δ 直接證明。



S08 · implies操作前

f_4\ \text{continuous at}\ 1\ \text{(assumed)},\ \varepsilon=\tfrac12,\ x=1-\tfrac{\delta}{2}

操作後

|f_4(x)-4|=|(3-\delta)-4|=1+\delta>\tfrac12:\ \text{contradiction}

條件：\delta>0

規則：contradiction · 依賴：S01, G2

葉節點依據：contradiction + exists_elim + abs_rules + order_basics

反證：假設 f_4 在 1 連續。對 ε=1/2 取得某個 δ>0。令 x=1−δ/2，則 |x−1|=δ/2<δ 且 x<1，所以 f_4(x)=2(1−δ/2)+1=3−δ，|f_4(x)−f_4(1)|=|(3−δ)−4|=|−1−δ|=1+δ>1/2（N6）。這與連續性給出的 <1/2 矛盾，所以 f_4 在 1 不連續。



S09 · implies操作前

g:\ L^-=2\cdot1+1=3,\ L^+=5\cdot1-1=4,\ V=3

操作後

(L^- - V,\ L^+ - V)=(0,1)\neq(0,0)

條件：無

規則：mko_continuity · 依賴：G3, mko_continuity

葉節點依據：mko_continuity + numeric_evaluation

g 的左極限 3、右極限 4（N7），中心值 3。缺陷對 (0,1)：中心值只等於左側，右側不同，依判準不連續。



S10 · implies操作前

g\ \text{continuous at}\ 1\ \text{(assumed)},\ \varepsilon=\tfrac12,\ x=1+\tfrac{\delta}{2}

操作後

|g(x)-3|=1+\tfrac{5\delta}{2}>\tfrac12:\ \text{contradiction}

條件：\delta>0

規則：contradiction · 依賴：S01, G3

葉節點依據：contradiction + exists_elim + abs_rules + order_basics

假設 g 在 1 連續，對 ε=1/2 取得 δ>0。令 x=1+δ/2（x>1、|x−1|<δ），g(x)=5(1+δ/2)−1=4+5δ/2，|g(x)−g(1)|=1+5δ/2>1/2（N9），矛盾。所以 g 在 1 不連續，雖然 g(1) 等於左極限。



S11 · equivalent操作前

q(x)=\frac{x^2-4}{x-2},\ x\neq 2

操作後

q(x)=x+2\ (x\neq 2);\ 2\notin\mathrm{dom}(q)

條件：x-2\neq 0

規則：frac_rules · 依賴：G4, distributive, frac_rules

葉節點依據：frac_rules + distributive + mul_inverse_nonzero

x²−4=(x−2)(x+2)（N10），x≠2 時約去 x−2≠0，得 q(x)=x+2。q 的論域是 ℝ∖{2}，它不是 ℝ 上的函數，所以在本模型中「q 在 2 連續」沒有意義；有意義的問題是：怎樣的全實數延拓 F_W 在 2 連續。



S12 · implies操作前

W=4:\ |F_4(x)-4|

操作後

|x-2|\ \text{for every}\ x;\ \delta=\varepsilon\ \Rightarrow\ F_4\ \text{continuous at}\ 2

條件：無

規則：forall_intro · 依賴：S01, S11, G4

葉節點依據：forall_intro + exists_intro + continuity_def + case_analysis

存在性：W=4 時，x≠2 有 F_4(x)−4=(x+2)−4=x−2，x=2 有 F_4(2)−4=0=2−2；所以對所有 x，|F_4(x)−F_4(2)|=|x−2|。對任意 ε>0 取 δ=ε 即得連續。



S13 · implies操作前

F_W\ \text{continuous at}\ 2

操作後

W=4

條件：無

規則：L_unique_ext · 依賴：S11, S12

葉節點依據：contradiction + abs_rules + order_basics

唯一性：依引理 L_unique_ext，任何在 2 連續的延拓都必須取 W=4。與 MKO 的「唯一所需值為 2a」一致（a=2）。引理在 S13.1 至 S13.3 以反證證明。



S14 · implies操作前

\text{S06, S08, S10, S12, S13}

操作後

f_3\ \text{cont.},\ f_4,\ g\ \text{not};\ F_W\ \text{cont. at 2}\iff W=4

條件：無

規則：and_intro_elim · 依賴：S06, S08, S10, S12, S13

葉節點依據：and_intro_elim + iff_intro

匯總：V=3 連續、V=4 不連續、g 不連續；可去商的延拓在 2 連續當且僅當 W=4（S12 給出 ⇐，S13 給出 ⇒）。原商 q 仍只在 ℝ∖{2} 上有定義。







## 局部子步與引理

S05.1 · implies操作前

x<1:\ |f_3(x)-3|

操作後

|2x-2|=2|x-1|\le 5|x-1|

條件：x<1

規則：abs_rules · 依賴：G2, abs_rules

葉節點依據：abs_rules + distributive + order_basics

x<1 時 f_3(x)=2x+1，(2x+1)−3=2(x−1)（N3），絕對值 2|x−1|；又 |x−1|≥0，所以 2|x−1|≤5|x−1|。



S05.2 · implies操作前

x>1:\ |f_3(x)-3|

操作後

|5x-5|=5|x-1|

條件：x>1

規則：abs_rules · 依賴：G2, abs_rules

葉節點依據：abs_rules + distributive

x>1 時 f_3(x)=5x−2，(5x−2)−3=5(x−1)（N4），絕對值 5|x−1|。



S05.3 · implies操作前

x=1:\ |f_3(1)-3|

操作後

|3-3|=0=5|1-1|

條件：x=1

規則：numeric_evaluation · 依賴：G2

葉節點依據：numeric_evaluation + abs_rules

x=1 時 f_3(1)=V=3，差為 0，等於 5|1−1|=0。中心點也滿足界；這一情況只有在 V=3 時成立。三個情況合起來證得引理 L_branch_bound。



S13.1 · implies操作前

W\neq 4\ \text{(assumed)},\ F_W\ \text{continuous at}\ 2

操作後

\varepsilon=\tfrac{|W-4|}{2}>0,\ \delta>0:\ |x-2|<\delta\Rightarrow|F_W(x)-W|<\varepsilon

條件：W\neq 4

規則：exists_elim · 依賴：continuity_def, exists_elim

葉節點依據：exists_elim + continuity_def + abs_rules

假設 W≠4 且 F_W 在 2 連續。|W−4|>0，所以 ε=|W−4|/2>0；依連續性定義取得某個 δ>0。



S13.2 · implies操作前

r=\tfrac12\min(\delta,\varepsilon),\ x=2+r

操作後

|F_W(x)-W|<\varepsilon,\ |F_W(x)-4|=r<\varepsilon

條件：r>0

規則：forall_elim · 依賴：S13.1, S11

葉節點依據：forall_elim + order_basics + eq_replace

令 r=min(δ,ε)/2>0，x=2+r。則 |x−2|=r<δ，由 S13.1，|F_W(x)−W|<ε；又 x≠2，F_W(x)=x+2=4+r，所以 |F_W(x)−4|=r<ε。



S13.3 · implies操作前

|W-4|\le|W-F_W(x)|+|F_W(x)-4|

操作後

|W-4|<2\varepsilon=|W-4|:\ \text{contradiction, so}\ W=4

條件：無

規則：contradiction · 依賴：S13.2, abs_rules

葉節點依據：contradiction + abs_rules + order_basics

三角不等式：|W−4|≤|W−F_W(x)|+|F_W(x)−4|<ε+ε=2ε=|W−4|，得 |W−4|<|W−4|，矛盾（例如 W=5 時 2·(1/2)=1=|5−4|，N12）。所以假設 W≠4 不成立，W=4。S13.1 至 S13.3 證得引理 L_unique_ext。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S06, S08, S10, S12, S13 — 目標 G：本稿的四個結論。每一部分已正向證成；W=4 的雙向分別來自 S12 與 S13。
- S13.3 · premise_audit · S13.2, abs_rules, contradiction — 矛盾只否定 W≠4；存在性另由 S12 證明。
- S13.2 · premise_audit · S13.1, S11, forall_elim — 取 x≠2 是為了使用 q 的公式；r 同時小於 δ 與 ε。
- S13.1 · premise_audit · continuity_def, exists_elim, abs_rules — 需要 W≠4 才能使 ε>0。
- S13 · premise_audit · L_unique_ext — 引理只用 x≠2 的值 x+2 與連續性定義，不引用極限唯一性的一般定理。
- S12 · premise_audit · S01, S11, forall_intro — 兩種 x 都檢查了；ε 任意。
- S11 · inverse_equivalence · frac_rules, distributive — 在論域 x≠2 上雙向成立；不延伸到 x=2。
- S10 · premise_audit · S01, exists_elim, contradiction — 與 S08 同理；只需右側一點。
- S09 · premise_audit · G3, mko_continuity, numeric_evaluation — 缺陷對的讀法；獨立反證在 S10。
- S08 · premise_audit · S01, exists_elim, contradiction, abs_rules — δ 是由假設取出的任意正數；論證對每個可能的 δ 都成立，所以結論不依賴 δ。
- S07 · premise_audit · S03, S04, numeric_evaluation — 缺陷對只是判準的讀法；獨立的反證在 S08。
- S06 · sufficient_goal_reduction · S01, S05, forall_intro — 目標 G：f_3 在 1 連續。足夠條件 H：對任意 ε，δ=ε/5 有效；H⇒G 由定義。H 由 S05 正向證成，未把 G 當作前提。
- S05.3 · premise_audit · numeric_evaluation — 若 V=4，此情況給出 1≤0，不成立，所以引理只對 V=3 宣稱。
- S05.2 · premise_audit · abs_rules, distributive — 等式自然也是 ≤ 的情形。
- S05.1 · premise_audit · abs_rules, order_basics — 只宣稱不超過；2 與 5 的比較需要 |x−1|≥0。
- S05 · premise_audit · L_branch_bound, case_analysis — 三個情況互斥且涵蓋全部 x（S02）。
- S04 · premise_audit · S03, mko_continuity — 判準引自 MKO；本稿在 S06 與 S08 對 V=3、V=4 各自獨立驗證。
- S03 · inverse_equivalence · numeric_evaluation — 精確求值，兩邊是同一個數。
- S02 · premise_audit · G2, function_def, order_basics — 用到實數三分律保證三個情況恰有其一。
- S01 · premise_audit · G1, mko_continuity, continuity_def — 此步只展開定義。





## 錯誤控制與反例

左右極限相等仍不足MKO 的誤解之一是左右極限相等就忽略點值。f_4 的左右極限都是 3，但 f_4(1)=4，S08 以 ε=1/2 直接證明它不連續。連續要求的是「兩側極限 = 中心值」，中心值是判定的一部分。

中心值只配合一側也不夠g(1)=3 等於左極限，但右極限是 4（S09、S10），所以不連續。點缺陷對 (L⁻−V, L⁺−V) 兩個分量都必須為 0。

可去不等於不需補定另一個誤解是未補定便聲稱原商在中心連續。q 在 2 沒有定義（S11），談不上在 2 連續；要得到全實數連續函數必須補值，而且只有 W=4 可行（S12、S13）。補了其他值（例如 W=0）的延拓在 2 不連續。


- f_4 的左右極限都是 3，所以 f_4 在 1 連續 → reject — f_4(1)=4≠3；x=1−δ/2 給出誤差 1+δ>1/2（S08）。
- g(1)=3 等於左極限，所以 g 在 1 連續 → reject — 右極限為 4；x=1+δ/2 給出誤差 1+5δ/2>1/2（S10）。
- q(x)=(x²−4)/(x−2) 在 2 的極限是 4，所以 q 在 2 連續 → reject — q 在 2 無定義；只有補值 W=4 的延拓 F_4 在 2 連續。
- 可去奇點補任何值都能得到連續延拓，例如 F(2)=0 → reject — S13 證明必須 W=4；W=0 時取 ε=2 即可否定連續。
- 檢查 f_3(0.9) 與 f_3(1.1) 都接近 3，就證明了 f_3 在 1 連續 → reject — 有限測點不是證明；證明是 S06 對任意 ε 的論證。





## 結論與限制

f_V 的左右極限都是 3：V=3 時在 1 連續（δ=ε/5），V=4 時不連續（缺陷對 (−1,−1)）。g 的左右極限 3、4 不等，中心值 3 只配合左側，所以不連續（缺陷對 (0,1)）。q=(x²−4)/(x−2) 只在 ℝ∖{2} 有定義；全實數延拓在 2 連續當且僅當補值 W=4。


- MKO 的判準「左極限=右極限=V ⇔ 連續」在本稿中被引用，並在兩個具體情況下以 ε-δ 獨立核對；一般等價的證明不在本稿範圍。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 47982f7ca8622e26e45615f6dc3a8550fa228ca562132006c98685246f8606e4
- original source SHA-256: 47982f7ca8622e26e45615f6dc3a8550fa228ca562132006c98685246f8606e4
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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