函數極限：可去因子商、仿射 δ 界與不等的單側極限

目標與範圍

在去心實數論域上：(1) 以 ε-δ 證明 f(x)=(x²−9)/(x−3) 滿足 lim_(x→3) f(x)=6，而 f(3) 仍無定義；(2) 對仿射 g(x)=4x−1 在 a=2、ε=1/2，證明 δ=1/8 合法（等號 |m|δ=ε 允許），δ=1/7 不合法；(3) 對分支函數 h(x)=x+1（x<1）、h(x)=2x+3（x>1），求左右極限 2 與 5，並證明兩側極限不存在。

只處理 MKO 的三類題：仿射式、可去因子商、左右仿射分支，論域為 ℝ∖{a}。不證明一般極限定律（和、積、合成），不處理孤立點或其他接近論域。不改動 canonical MKO 或英文 edition。

已知條件與符號

• abs_rules
• order_basics
• frac_rules
• distributive
• func_limit_def
• numeric_evaluation

• G1 — 函數定義在去心論域 ℝ∖{a} 上；不要求 f(a) 存在。
• G2 — f(x)=(x²−9)/(x−3)，論域 ℝ∖{3}。
• G3 — g(x)=4x−1（m=4、b=−1），a=2；ε=1/2（p=1、q=2）；候選 δ=1/8（u=1、v=8）與 δ=1/7。
• G4 — h(x)=x+1（x<1），h(x)=2x+3（x>1），論域 ℝ∖{1}。

• \lim_{x\to a}f(x)=L — 去心兩側極限
• \varepsilon,\ \delta — 輸出容差與輸入距離界，皆為正
• 0<|x-a|<\delta — 去心鄰域：x≠a 且距離嚴格小於 δ
• \varepsilon=\tfrac{p}{q},\ \delta=\tfrac{u}{v} — 有理容差與有理距離界
• L^-,\ L^+ — 左極限與右極限

規則與來源

• 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。
• 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）。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• func_limit_def · prerequisite — 函數極限：lim_{x→a} f(x)=L 表示對每個 ε>0，存在 δ>0，使所有滿足 0<|x−a|<δ 的定義域點 x 都有 |f(x)−L|<ε（a 須為定義域的極限點）。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_func_limit · cited — 對在 a 附近所有 x≠a 都有定義的實函數 f，lim_(x→a) f(x)=L 指每個 ε>0 都有 δ>0，使 0<|x−a|<δ 時 |f(x)−L|<ε；左右有限極限必須相等才有兩側極限。仿射 mx+b 的極限為 ma+b；ε=p/q、δ=u/v 的仿射均勻界允許 |m|uq≤pv，等號合法。 · mko-function-limit
• one_sided_def · prerequisite — 左極限 L⁻：每個 ε>0 都有 δ>0，使 a−δ<x<a 時 |f(x)−L⁻|<ε；右極限 L⁺：a<x<a+δ 時 |f(x)−L⁺|<ε。
• L_affine_bound · lemma — 對 g(x)=mx+b、實數 a、ε>0、δ>0：若 |m|δ≤ε，則 0<|x−a|<δ 推出 |g(x)−(ma+b)|<ε。

逐步主鏈

\lim_{x\to a}f(x)=L

\forall\varepsilon>0\ \exists\delta>0\ \forall x:\ 0<|x-a|<\delta\Rightarrow|f(x)-L|<\varepsilon

\mathrm{dom}(f)=\mathbb{R}\setminus\{3\}

\forall\delta>0:\ \{x:0<|x-3|<\delta\}\subseteq\mathrm{dom}(f),\ 3+\tfrac{\delta}{2}\ \text{in it}

x^2-9

(x-3)(x+3)

f(x)=\frac{(x-3)(x+3)}{x-3}\ (x\neq 3)

f(x)=x+3\ (x\neq 3)

|f(x)-6|\ (x\neq 3)

|(x+3)-6|=|x-3|

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

0<|x-3|<\delta\Rightarrow|f(x)-6|=|x-3|<\varepsilon;\ \lim_{x\to 3}f(x)=6

|g(x)-7|,\ g(x)=4x-1,\ 7=4\cdot 2-1

|4x-8|=|4(x-2)|=4|x-2|

|m|\cdot\frac{u}{v}\le\frac{p}{q}

|m|\,u\,q\le p\,v

4\cdot 1\cdot 2=8\le 8=1\cdot 8

0<|x-2|<\tfrac18\Rightarrow|g(x)-7|<\tfrac12

\delta=\tfrac17:\ 4\cdot 1\cdot 2=8>7=1\cdot 7

x=2+\tfrac18:\ 0<|x-2|<\tfrac17,\ |g(x)-7|=\tfrac12\not<\tfrac12

x<1:\ |h(x)-2|

|(x+1)-2|=|x-1|;\ \delta=\varepsilon\ \text{gives}\ L^-=2

x>1:\ |h(x)-5|

|(2x+3)-5|=2|x-1|;\ \delta=\tfrac{\varepsilon}{2}\ \text{gives}\ L^+=5

\lim_{x\to 1}h(x)=L\ \text{(assumed)},\ \varepsilon=\tfrac32

\delta>0,\ t=\tfrac{\delta}{2}:\ |h(1+t)-L|<\tfrac32,\ |h(1-t)-L|<\tfrac32

|h(1+t)-h(1-t)|\le|h(1+t)-L|+|L-h(1-t)|<3

h(1+t)-h(1-t)=3+3t>3:\ \text{contradiction};\ \lim_{x\to 1}h(x)\ \text{does not exist}

\text{S06, S09, S10, S11, S12, S14}

\lim_{x\to3}f=6;\ \delta=\tfrac18\ \text{valid},\ \tfrac17\ \text{not};\ L^-=2\neq 5=L^+,\ \text{no two-sided limit}

局部子步與引理

|(mx+b)-(ma+b)|

|m(x-a)|=|m|\,|x-a|

m=0

|g(x)-(ma+b)|=0<\varepsilon\ \text{for every}\ x

m\neq 0,\ 0<|x-a|<\delta,\ |m|\delta\le\varepsilon

|m||x-a|<|m|\delta\le\varepsilon

逐步反向審查

• S15 · sufficient_goal_reduction · S06, S09, S10, S11, S12, S14 — 目標 G：本稿的三個結論。每一部分已由所列步驟正向證成；本步只合取，未把 G 當作前提。
• S14 · premise_audit · S13, abs_rules, contradiction — 矛盾只否定了「兩側極限存在」這個假設；S11、S12 的單側極限不受影響。
• S13 · premise_audit · S01, exists_elim, forall_elim — δ 是由假設取出的新名字；之後的結論不含 δ。
• S12 · premise_audit · G4, one_sided_def, forall_intro — 只用右分支在 x>1 的公式；兩個單側極限各自存在。
• S11 · premise_audit · G4, one_sided_def, forall_intro — 只用左分支在 x<1 的公式；ε 任意。
• S10 · premise_audit · S07, quantifier_negation, numeric_evaluation — 判準失敗本身只說明引理不適用；不合法的結論來自具體反例（N6、N7、N8）。
• S09.3 · premise_audit · S09.1, order_basics — 需要 |m|>0 才能保持嚴格不等號；m=0 已在 S09.2 另行處理。
• S09.2 · premise_audit · S09.1, mul_zero — 只需 ε>0；這是引理的第一個情況。
• S09.1 · inverse_equivalence · distributive, abs_rules — 恆等式，雙向成立。
• S09 · premise_audit · S08, L_affine_bound, numeric_evaluation — 引理的前提 |m|δ≤ε 以 N4、N5 核對；引理只給出充分條件。
• S08 · inverse_equivalence · order_basics, frac_rules — 反向是同除以正數 qv。
• S07 · inverse_equivalence · abs_rules, distributive — 恆等變形，雙向成立。
• S06 · sufficient_goal_reduction · S01, S05, forall_intro — 目標 G：極限為 6。足夠條件 H：對任意 ε，δ=ε 有效；H⇒G 由定義。H 由 S05 正向證成，未把 G 當作前提，也沒有用到 f(3)。
• S05 · inverse_equivalence · S04, eq_replace — 等值代換，雙向成立；只在 x≠3 使用。
• S04 · inverse_equivalence · frac_rules, mul_inverse_nonzero — 反向是分子分母同乘 x−3，需要 x−3≠0；條件在論域內處處成立。
• S03 · inverse_equivalence · distributive — 恆等式，雙向成立。
• S02 · premise_audit · G2, S01, order_basics — 只確認極限問題有意義（3 是論域的極限點）；不宣稱極限存在。
• S01 · premise_audit · G1, mko_func_limit, func_limit_def — 此步只展開定義，不推出新事實。

錯誤控制與反例

分清極限與 f(a)，不能除零後補值

MKO 的誤解之一是把極限當 f(a)。f(3) 是 0/0，沒有定義；極限 6 來自 x≠3 處的化簡 f(x)=x+3（S04），而 0<|x−3| 把中心排除在外（S01）。化簡不等於在 3 定義了 f；若另外定義 f(3)=100，極限仍是 6。

δ 邊界的等號合法

另一個誤解是把 |m|δ=ε 當成不合法。因為輸入距離嚴格小於 δ，4|x−2|<4δ=ε 仍是嚴格的（S09.3），所以 δ=1/8 合法。這和數列尾界不同：那裡比較的是誤差本身，誤差等於 ε 不合格。δ=1/7 不合法則要用具體反例證明（S10）。

單側極限不等只否定兩側極限

h 的左右極限 2 與 5 都存在，只是不等，所以兩側極限不存在（S14）。這不表示右極限不存在，也不能用有限個測點（例如 x=0.9、1.1）代替 ε-δ 論證。

• f(3)=0/0 沒有定義，所以 lim_(x→3) f(x) 不存在 → reject — 去心極限不看 f(3)；S06 證得極限為 6。
• f(x)=x+3，所以 f(3)=6 → reject — 化簡只在 x≠3 成立；f 的論域是 ℝ∖{3}，在 3 約分要除以 0。
• ε=1/2 時 δ=1/8 不合法，因為 |m|δ 恰等於 ε → reject — 0<|x−2|<1/8 給出 4|x−2|<1/2，嚴格不等成立。
• h 在 1 的兩側極限不存在，所以右極限也不存在 → reject — 右極限為 5（S12）；只是不等於左極限 2。
• f(3.1)=6.1、f(2.9)=5.9，所以極限為 6 已得證 → reject — 有限測點只與結論相容，不是證明；證明是 S06 對任意 ε 的論證。

結論與限制

f(x)=(x²−9)/(x−3) 在 ℝ∖{3} 上滿足 lim_(x→3) f(x)=6（δ=ε），而 f(3) 仍無定義。g(x)=4x−1 在 a=2、ε=1/2：δ=1/8 合法（4·1·2=8≤8，等號允許），δ=1/7 不合法（x=2+1/8 的誤差恰為 1/2）。h 的左極限為 2、右極限為 5，兩側極限不存在。

• 本稿不證明一般極限定律，也不處理論域含孤立點的情形。
• N2 是兩個測點的數值核對，只與 S04 的化簡相容，不參與證明。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: f75050de6a74ead986b8699e576b6dd6e5e0acae0be6646bdbb41b727c4ac99e
• original source SHA-256: f75050de6a74ead986b8699e576b6dd6e5e0acae0be6646bdbb41b727c4ac99e
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）