# Function limits: a removable-factor quotient, affine δ bounds and unequal one-sided limits

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-function-limit/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-function-limit-01 · production-20261019-adopted-96



## Goal and scope

On punctured real domains: (1) prove by ε-δ that f(x)=(x²−9)/(x−3) has lim_(x→3) f(x)=6 while f(3) stays undefined; (2) for the affine g(x)=4x−1 at a=2 with ε=1/2, prove that δ=1/8 is valid (the equality |m|δ=ε is allowed) and δ=1/7 is not; (3) for the branch function h(x)=x+1 (x<1), h(x)=2x+3 (x>1), find the one-sided limits 2 and 5 and prove that the two-sided limit does not exist.

Treats only the MKO's three kinds of exercise: affine expressions, removable-factor quotients and left/right affine branches, on the domain ℝ∖{a}. It does not prove general limit laws (sums, products, composition) and does not treat isolated points or other approach domains. It does not change the canonical MKO or its English edition.





## Givens and symbols


- abs_rules
- order_basics
- frac_rules
- distributive
- func_limit_def
- numeric_evaluation


- G1 — Functions are defined on the punctured domain ℝ∖{a}; f(a) need not exist.
- G2 — f(x)=(x²−9)/(x−3) on ℝ∖{3}.
- G3 — g(x)=4x−1 (m=4, b=−1), a=2; ε=1/2 (p=1, q=2); candidate δ=1/8 (u=1, v=8) and δ=1/7.
- G4 — h(x)=x+1 for x<1 and h(x)=2x+3 for x>1, on ℝ∖{1}.


- \lim_{x\to a}f(x)=L — the punctured two-sided limit
- \varepsilon,\ \delta — the output tolerance and the input distance bound, both positive
- 0<|x-a|<\delta — the punctured neighbourhood: x≠a and distance strictly below δ
- \varepsilon=\tfrac{p}{q},\ \delta=\tfrac{u}{v} — rational tolerance and rational distance bound
- L^-,\ L^+ — the left and right limits





## Rules and sources


- abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- func_limit_def · prerequisite — Limit of a function: lim_{x→a} f(x)=L means that for every ε>0 there is δ>0 such that |f(x)−L|<ε for every domain point x with 0<|x−a|<δ (a must be a limit point of the domain).
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- add_zero · prerequisite — Additive identity: u+0=u.
- mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_func_limit · cited — For a real f defined at all x≠a near a, lim_(x→a) f(x)=L means each ε>0 admits δ>0 with |f(x)−L|<ε whenever 0<|x−a|<δ; a finite two-sided limit requires equal one-sided limits. The affine limit of mx+b is ma+b; for ε=p/q and δ=u/v the uniform affine bound permits |m|uq≤pv, equality included. · mko-function-limit
- one_sided_def · prerequisite — Left limit L⁻: each ε>0 admits δ>0 with |f(x)−L⁻|<ε whenever a−δ<x<a; right limit L⁺: the same with a<x<a+δ.
- L_affine_bound · lemma — For g(x)=mx+b, a real a, ε>0 and δ>0: if |m|δ≤ε, then 0<|x−a|<δ implies |g(x)−(ma+b)|<ε.





## Main derivation

S01 · definitionBefore

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

After

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

Conditions: none

Rule: mko_func_limit · Uses: G1, func_limit_def

Leaf basis: func_limit_def + def_unfold

Unfold the punctured limit by the MKO. The condition 0<|x−a|<δ excludes x=a, so whether f(a) exists, and its value, never enters the definition; the input distance is strictly below δ and the output error strictly below ε.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: mko_func_limit · Uses: G2, S01

Leaf basis: set_builder + order_basics

Every x in a punctured neighbourhood has x≠3, so it lies in the domain of f; and 3+δ/2 belongs to it (0<δ/2<δ), so the neighbourhood is not empty. Hence 'the limit of f as x→3' is a meaningful question, even though f(3)=(9−9)/(3−3) is 0/0 and undefined.



S03 · equivalentBefore

x^2-9

After

(x-3)(x+3)

Conditions: none

Rule: distributive · Uses: G2, distributive

Leaf basis: distributive + add_inverse + add_zero

Distributivity expands (x−3)(x+3)=x²+3x−3x−9=x²−9, an identity for every real x (N1).



S04 · equivalentBefore

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

After

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

Conditions: x-3\neq 0

Rule: frac_rules · Uses: S03, frac_rules

Leaf basis: frac_rules + mul_inverse_nonzero

For x≠3, x−3≠0, so the common factor cancels: (x+3)(x−3)/(1·(x−3))=(x+3)/1 (a/b=(ak)/(bk) with k=x−3≠0). This holds only on the domain ℝ∖{3}; it gives f no value at 3, since cancelling there would divide by 0.



S05 · equivalentBefore

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

After

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

Conditions: x\neq 3

Rule: eq_replace · Uses: S04

Leaf basis: eq_replace + add_assoc + add_inverse

At x≠3 substitute f(x)=x+3 from S04; (x+3)−6=x−3. The output error equals the input distance exactly.



S06 · impliesBefore

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

After

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

Conditions: \varepsilon>0

Rule: forall_intro · Uses: S01, S02, S05

Leaf basis: forall_intro + exists_intro + func_limit_def

Take an arbitrary ε>0 and set δ=ε>0. If 0<|x−3|<δ then x≠3, and by S05 |f(x)−6|=|x−3|<δ=ε. As ε is arbitrary, generalization and S01 give lim_(x→3) f(x)=6. The limit 6 is not f(3): f(3) is still undefined (S02).



S07 · equivalentBefore

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

After

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

Conditions: none

Rule: abs_rules · Uses: G3, abs_rules

Leaf basis: abs_rules + distributive + numeric_evaluation

The affine limit value is ma+b=4·2−1=7 (MKO assumption a2). g(x)−7=4x−8=4(x−2) (N3), and by |uv|=|u||v|, |g(x)−7|=4|x−2|.



S08 · equivalentBefore

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

After

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

Conditions: q>0; v>0

Rule: order_basics · Uses: G3, frac_rules

Leaf basis: order_basics + frac_rules

Multiply both sides by the positive qv; the direction is unchanged, giving the integer criterion |m|uq≤pv, the form of MKO assumption a3. Here it is '≤': equality is allowed.



S09 · theorem_applicationBefore

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

After

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

Conditions: |m|\delta\le\varepsilon

Rule: L_affine_bound · Uses: S07, S08, G3

Leaf basis: abs_rules + order_basics + case_analysis

Substitute m=4, u=1, v=8, p=1, q=2: |m|uq=8≤8=pv, with equality, that is |m|δ=4·(1/8)=1/2=ε. By Lemma L_affine_bound, δ=1/8 is valid. Equality is fine because the input distance is strictly below δ: 4|x−2|<4·(1/8)=1/2. The lemma is proved in S09.1 to S09.3.



S10 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: S07, S08, G3

Leaf basis: quantifier_negation + numeric_evaluation + order_basics

For δ=1/7 the criterion 8≤7 fails. The lemma then does not apply, and it must still be shown that δ=1/7 really fails: take x=2+1/8; then |x−2|=1/8<1/7 and x≠2, while |g(x)−7|=4·(1/8)=1/2, not below ε=1/2. One counterexample refutes 'every x with 0<|x−2|<1/7 qualifies'.



S11 · impliesBefore

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

After

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

Conditions: x<1

Rule: one_sided_def · Uses: G4, one_sided_def

Leaf basis: one_sided_def + abs_rules + forall_intro

On the left, x<1, h(x)=x+1 and (x+1)−2=x−1 (N9). For arbitrary ε>0 take δ=ε: if 1−δ<x<1 then |h(x)−2|=|x−1|<δ=ε. So the left limit is 2, the value 1·1+1 of the left branch.



S12 · impliesBefore

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

After

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

Conditions: x>1

Rule: one_sided_def · Uses: G4, one_sided_def

Leaf basis: one_sided_def + abs_rules + forall_intro

On the right, x>1, h(x)=2x+3 and (2x+3)−5=2(x−1) (N10). Take δ=ε/2: if 1<x<1+δ then |h(x)−5|=2|x−1|<2δ=ε. So the right limit is 5, the value 2·1+3 of the right branch.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: exists_elim · Uses: S01, G4

Leaf basis: exists_elim + forall_elim + order_basics

By contradiction: suppose a two-sided limit L exists. For ε=3/2 the definition gives some δ>0. Let t=δ/2, so 0<t<δ and both points 1+t and 1−t satisfy 0<|x−1|<δ; hence |h(1+t)−L|<3/2 and |h(1−t)−L|<3/2. ε=3/2 is chosen because the one-sided limits differ by 3, and 3/2 is half of that.



S14 · impliesBefore

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

After

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

Conditions: t>0

Rule: contradiction · Uses: S13, abs_rules

Leaf basis: contradiction + abs_rules + order_basics + numeric_evaluation

The triangle inequality and |L−h(1−t)|=|h(1−t)−L| give |h(1+t)−h(1−t)|<3/2+3/2=3. But directly h(1+t)−h(1−t)=(2(1+t)+3)−((1−t)+1)=3+3t (N11), which exceeds 3 since t>0, and so does its absolute value. Contradiction, so the two-sided limit does not exist.



S15 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S06, S09, S10, S11, S12, S14

Leaf basis: and_intro_elim

Collect the three conclusions. For h, the one-sided limits 2 and 5 both exist legitimately but differ, so only the two-sided limit is denied; neither side may be erased, and h(1), which is undefined, cannot repair anything.







## Substeps and lemmas

S09.1 · equivalentBefore

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

After

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

Conditions: none

Rule: abs_rules · Uses: distributive, abs_rules

Leaf basis: distributive + abs_rules + add_inverse

(mx+b)−(ma+b)=mx−ma=m(x−a) (N13), then |uv|=|u||v|. This holds for every m, a, b, x.



S09.2 · impliesBefore

m=0

After

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

Conditions: m=0

Rule: mul_zero · Uses: S09.1, mul_zero

Leaf basis: mul_zero + order_basics

Case m=0: by S09.1 the error is 0·|x−a|=0<ε for every x, so every positive δ works (MKO assumption a3).



S09.3 · impliesBefore

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

After

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

Conditions: |m|>0

Rule: order_basics · Uses: S09.1, order_basics

Leaf basis: order_basics + case_analysis

Case m≠0: |m|>0, so multiplying the strict |x−a|<δ by the positive |m| gives |m||x−a|<|m|δ; with |m|δ≤ε, transitivity of order gives the strict |g(x)−(ma+b)|<ε. The strictness comes from the input's <δ, so the equality case |m|δ=ε is also valid. The two cases cover every m, and S09.1 to S09.3 prove Lemma L_affine_bound.







## Reverse audits


- S15 · sufficient_goal_reduction · S06, S09, S10, S11, S12, S14 — Goal G: the three conclusions of this guide. Each part is proved forwards by the listed steps; this step only conjoins them, without assuming G.
- S14 · premise_audit · S13, abs_rules, contradiction — The contradiction refutes only the assumption that a two-sided limit exists; the one-sided limits of S11 and S12 are unaffected.
- S13 · premise_audit · S01, exists_elim, forall_elim — δ is a fresh name taken from the assumption; the final conclusion does not mention δ.
- S12 · premise_audit · G4, one_sided_def, forall_intro — Only the right branch formula on x>1 is used; each one-sided limit exists on its own.
- S11 · premise_audit · G4, one_sided_def, forall_intro — Only the left branch formula on x<1 is used; ε is arbitrary.
- S10 · premise_audit · S07, quantifier_negation, numeric_evaluation — The failed criterion only means the lemma does not apply; invalidity comes from the explicit counterexample (N6, N7, N8).
- S09.3 · premise_audit · S09.1, order_basics — |m|>0 is needed to keep the strict inequality; m=0 is handled separately in S09.2.
- S09.2 · premise_audit · S09.1, mul_zero — Only ε>0 is needed; this is the first case of the lemma.
- S09.1 · inverse_equivalence · distributive, abs_rules — An identity, valid both ways.
- S09 · premise_audit · S08, L_affine_bound, numeric_evaluation — The lemma's hypothesis |m|δ≤ε is checked by N4 and N5; the lemma gives only a sufficient condition.
- S08 · inverse_equivalence · order_basics, frac_rules — Backward, divide by the positive qv.
- S07 · inverse_equivalence · abs_rules, distributive — Identities, valid both ways.
- S06 · sufficient_goal_reduction · S01, S05, forall_intro — Goal G: the limit is 6. Sufficient condition H: for arbitrary ε, δ=ε works; H⇒G by the definition. H is proved forwards from S05, without assuming G and without using f(3).
- S05 · inverse_equivalence · S04, eq_replace — Replacement of equals, valid both ways; used only at x≠3.
- S04 · inverse_equivalence · frac_rules, mul_inverse_nonzero — Backward, multiply numerator and denominator by x−3, which needs x−3≠0; the condition holds throughout the domain.
- S03 · inverse_equivalence · distributive — An identity, valid both ways.
- S02 · premise_audit · G2, S01, order_basics — It only confirms that the limit question is meaningful (3 is a limit point of the domain); it does not claim the limit exists.
- S01 · premise_audit · G1, mko_func_limit, func_limit_def — This step only unfolds the definition and derives no new fact.





## Error controls and negative controls

Distinguish the limit from f(a); do not patch a value in after division by zeroOne misconception the MKO lists is taking the limit to be f(a). f(3) is 0/0 and undefined; the limit 6 comes from the simplification f(x)=x+3 at x≠3 (S04), and 0<|x−3| keeps the centre out (S01). The simplification does not define f at 3; if one separately set f(3)=100, the limit would still be 6.

Equality at the δ boundary is allowedAnother misconception is rejecting |m|δ=ε. Because the input distance is strictly below δ, 4|x−2|<4δ=ε stays strict (S09.3), so δ=1/8 is valid. This differs from sequence cutoffs, where the error itself is compared and an error equal to ε fails. That δ=1/7 fails must be shown by an explicit counterexample (S10).

Unequal one-sided limits deny only the two-sided limitThe one-sided limits 2 and 5 of h both exist but differ, so there is no two-sided limit (S14). This does not mean the right limit fails to exist, and finitely many test points (for example x=0.9 and 1.1) cannot replace the ε-δ argument.


- f(3)=0/0 is undefined, so lim_(x→3) f(x) does not exist → reject — The punctured limit ignores f(3); S06 proves the limit is 6.
- f(x)=x+3, so f(3)=6 → reject — The simplification holds only at x≠3; the domain of f is ℝ∖{3}, and cancelling at 3 would divide by 0.
- For ε=1/2, δ=1/8 is invalid because |m|δ equals ε exactly → reject — 0<|x−2|<1/8 gives 4|x−2|<1/2, a strict inequality.
- h has no two-sided limit at 1, so its right limit does not exist either → reject — The right limit is 5 (S12); it merely differs from the left limit 2.
- f(3.1)=6.1 and f(2.9)=5.9, so the limit 6 is proved → reject — Finitely many test points are only consistent with the conclusion, not a proof; the proof is the argument of S06 for arbitrary ε.





## Result and limitations

f(x)=(x²−9)/(x−3) on ℝ∖{3} has lim_(x→3) f(x)=6 (with δ=ε), while f(3) stays undefined. For g(x)=4x−1 at a=2 with ε=1/2: δ=1/8 is valid (4·1·2=8≤8, equality allowed) and δ=1/7 is not (at x=2+1/8 the error is exactly 1/2). h has left limit 2 and right limit 5, and no two-sided limit.


- This guide does not prove general limit laws and does not treat domains with isolated points.
- N2 is a numerical check at two test points, consistent with the simplification of S04; it plays no part in the proof.





## Verification and source binding

14 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-function-limit-01.json)