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

目標與範圍

(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。

逐步主鏈

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_V\ \text{by three cases}

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

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

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

L^-=L^+=3

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

V=3

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

\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

V=4

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

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}

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

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

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}

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

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

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

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

F_W\ \text{continuous at}\ 2

W=4

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

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

局部子步與引理

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

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

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

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

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

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

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

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

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

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

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

逐步反向審查

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