# Continuity: centre values of branch functions and the unique continuous extension across a removable singularity

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

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-continuity-01 · production-20261019-adopted-96



## Goal and scope

(1) For f_V(x)=2x+1 (x<1), f_V(1)=V, f_V(x)=5x−2 (x>1), prove that f_V is continuous at 1 when V=3 and not when V=4; (2) for g(x)=2x+1 (x<1), g(1)=3, g(x)=5x−1 (x>1), prove that g is not continuous at 1; (3) for q(x)=(x²−4)/(x−2) on ℝ∖{2}, prove that a continuous extension to all real numbers must take the value 4 at 2, and that 4 does work.

Treats only the MKO's two-affine-branch model with an explicit centre value and extension of a quotient across a removable singularity, all argued directly by ε-δ and compared with the MKO's criterion 'left limit = right limit = V'. General continuity algebra and the intermediate value theorem are not proved. It does not change the canonical MKO or its English edition.





## Givens and symbols


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


- G1 — Functions f:ℝ→ℝ are defined on all reals, with the centre value stated explicitly.
- G2 — f_V(x)=2x+1 (x<1), f_V(1)=V, f_V(x)=5x−2 (x>1); compare V=3 and 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) on ℝ∖{2}; extension F_W(x)=q(x) for x≠2 and F_W(2)=W.


- f_V — the two-affine-branch function with centre value V
- L^-,\ L^+ — the left and right limits
- (L^- - V,\ L^+ - V) — the point-defect pair
- q — the removable quotient on ℝ∖{2}
- F_W — the extension of q to all real numbers with F_W(2)=W





## 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.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- 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.
- continuity_def · prerequisite — Continuity (ε-δ): f is continuous at a if for every ε>0 there is δ>0 such that |f(x)−f(a)|<ε for every domain point x with |x−a|<δ.
- 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.
- function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
- 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.
- 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).
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- 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.
- 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.
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- 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.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
- mko_continuity · cited — For f:ℝ→ℝ, continuity at a means every ε>0 admits δ>0 with |f(x)−f(a)|<ε whenever |x−a|<δ; equivalently the punctured two-sided limit equals the defined f(a). In the two-affine-branch model with explicit centre value V, continuity at a holds exactly when left limit = right limit = V. A continuous extension to all real numbers of the removable quotient needs the unique centre value 2a. · mko-continuity
- L_branch_bound · lemma — For every real x: |f_3(x)−3|≤5|x−1|.
- L_unique_ext · lemma — If F:ℝ→ℝ has F(x)=x+2 for x≠2 and F is continuous at 2, then F(2)=4.





## Main derivation

S01 · definitionBefore

f\ \text{continuous at}\ a

After

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

Conditions: f(a)\ \text{defined}

Rule: mko_continuity · Uses: G1, continuity_def

Leaf basis: continuity_def + def_unfold

Unfold continuity at a by the MKO. Unlike the punctured limit, the condition |x−a|<δ includes x=a, and the comparison is with the defined value f(a); so the centre value itself is part of the decision.



S02 · definitionBefore

f_V\ \text{by three cases}

After

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

Conditions: none

Rule: function_def · Uses: G2, function_def

Leaf basis: function_def + order_basics

The three cases x<1, x=1, x>1 are exclusive and cover all reals, so each x gets exactly one value and f_V is a function on ℝ; the centre value V is separate data, not determined by the branch formulas.



S03 · equivalentBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G2

Leaf basis: numeric_evaluation

By MKO assumption a2, the one-sided limit of an affine branch is the branch formula evaluated at a: left 2·1+1=3, right 5·1−2=3 (N1, N2). Neither depends on V.



S04 · theorem_applicationBefore

L^-=L^+=3

After

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

Conditions: none

Rule: mko_continuity · Uses: S03, mko_continuity

Leaf basis: mko_continuity

By the MKO's model criterion: continuous exactly when left limit = right limit = V. Both are 3, so the condition becomes V=3. Equivalently, the point-defect pair (3−V, 3−V) must be (0,0). S05 to S08 check both concrete cases directly by ε-δ, rather than relying only on this cited criterion.



S05 · impliesBefore

V=3

After

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

Conditions: none

Rule: L_branch_bound · Uses: G2, S02

Leaf basis: case_analysis + abs_rules + order_basics

By Lemma L_branch_bound, combining the three cases, the distance from f_3(x) to 3 is at most 5|x−1|. The lemma is proved by cases in S05.1 to S05.3.



S06 · impliesBefore

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

After

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

Conditions: \varepsilon>0

Rule: forall_intro · Uses: S01, S05

Leaf basis: forall_intro + exists_intro + order_basics + continuity_def

Take an arbitrary ε>0 and set δ=ε/5>0. If |x−1|<δ, then by S05 and f_3(1)=3, |f_3(x)−f_3(1)|≤5|x−1|<5δ=ε. As ε is arbitrary, S01 gives continuity of f_3 at 1, agreeing with the criterion of S04. For example ε=1/10 gives δ=1/50 (N11).



S07 · impliesBefore

V=4

After

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

Conditions: none

Rule: mko_continuity · Uses: S03, S04, G2

Leaf basis: mko_continuity + numeric_evaluation

With V=4 the point-defect pair is (3−4, 3−4)=(−1,−1) (N5), not (0,0). The one-sided limits agree (both 3) but differ from the centre value, so by the criterion of S04 the function is not continuous. S08 proves this directly by ε-δ.



S08 · impliesBefore

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

After

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

Conditions: \delta>0

Rule: contradiction · Uses: S01, G2

Leaf basis: contradiction + exists_elim + abs_rules + order_basics

By contradiction: suppose f_4 is continuous at 1. For ε=1/2 obtain some δ>0. Let x=1−δ/2; then |x−1|=δ/2<δ and x<1, so f_4(x)=2(1−δ/2)+1=3−δ and |f_4(x)−f_4(1)|=|(3−δ)−4|=|−1−δ|=1+δ>1/2 (N6). This contradicts the <1/2 given by continuity, so f_4 is not continuous at 1.



S09 · impliesBefore

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

After

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

Conditions: none

Rule: mko_continuity · Uses: G3, mko_continuity

Leaf basis: mko_continuity + numeric_evaluation

g has left limit 3 and right limit 4 (N7), with centre value 3. The defect pair is (0,1): the centre value matches only the left side, the right differs, so by the criterion g is not continuous.



S10 · impliesBefore

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

After

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

Conditions: \delta>0

Rule: contradiction · Uses: S01, G3

Leaf basis: contradiction + exists_elim + abs_rules + order_basics

Suppose g is continuous at 1 and obtain δ>0 for ε=1/2. Let x=1+δ/2 (x>1, |x−1|<δ); g(x)=5(1+δ/2)−1=4+5δ/2 and |g(x)−g(1)|=1+5δ/2>1/2 (N9), a contradiction. So g is not continuous at 1, although g(1) equals the left limit.



S11 · equivalentBefore

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

After

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

Conditions: x-2\neq 0

Rule: frac_rules · Uses: G4, distributive, frac_rules

Leaf basis: frac_rules + distributive + mul_inverse_nonzero

x²−4=(x−2)(x+2) (N10); for x≠2 cancel x−2≠0 to get q(x)=x+2. The domain of q is ℝ∖{2}; q is not a function on ℝ, so in this model 'q is continuous at 2' has no meaning. The meaningful question is which extension F_W to all real numbers is continuous at 2.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: forall_intro · Uses: S01, S11, G4

Leaf basis: forall_intro + exists_intro + continuity_def + case_analysis

Existence: with W=4, for x≠2, F_4(x)−4=(x+2)−4=x−2, and at x=2, F_4(2)−4=0=2−2; so |F_4(x)−F_4(2)|=|x−2| for all x. Taking δ=ε for arbitrary ε>0 gives continuity.



S13 · impliesBefore

F_W\ \text{continuous at}\ 2

After

W=4

Conditions: none

Rule: L_unique_ext · Uses: S11, S12

Leaf basis: contradiction + abs_rules + order_basics

Uniqueness: by Lemma L_unique_ext, every extension continuous at 2 must take W=4, agreeing with the MKO's 'the unique value is 2a' (a=2). The lemma is proved by contradiction in S13.1 to S13.3.



S14 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S06, S08, S10, S12, S13

Leaf basis: and_intro_elim + iff_intro

Summary: V=3 continuous, V=4 not, g not; the extension of the removable quotient is continuous at 2 exactly when W=4 (S12 gives ⇐, S13 gives ⇒). The original quotient q is still defined only on ℝ∖{2}.







## Substeps and lemmas

S05.1 · impliesBefore

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

After

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

Conditions: x<1

Rule: abs_rules · Uses: G2, abs_rules

Leaf basis: abs_rules + distributive + order_basics

For x<1, f_3(x)=2x+1 and (2x+1)−3=2(x−1) (N3), with absolute value 2|x−1|; as |x−1|≥0, 2|x−1|≤5|x−1|.



S05.2 · impliesBefore

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

After

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

Conditions: x>1

Rule: abs_rules · Uses: G2, abs_rules

Leaf basis: abs_rules + distributive

For x>1, f_3(x)=5x−2 and (5x−2)−3=5(x−1) (N4), with absolute value 5|x−1|.



S05.3 · impliesBefore

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

After

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

Conditions: x=1

Rule: numeric_evaluation · Uses: G2

Leaf basis: numeric_evaluation + abs_rules

At x=1, f_3(1)=V=3 and the difference is 0, equal to 5|1−1|=0. The centre also satisfies the bound; this case holds only because V=3. The three cases together prove Lemma L_branch_bound.



S13.1 · impliesBefore

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

After

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

Conditions: W\neq 4

Rule: exists_elim · Uses: continuity_def, exists_elim

Leaf basis: exists_elim + continuity_def + abs_rules

Suppose W≠4 and F_W is continuous at 2. Then |W−4|>0, so ε=|W−4|/2>0; the definition of continuity supplies some δ>0.



S13.2 · impliesBefore

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

After

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

Conditions: r>0

Rule: forall_elim · Uses: S13.1, S11

Leaf basis: forall_elim + order_basics + eq_replace

Let r=min(δ,ε)/2>0 and x=2+r. Then |x−2|=r<δ, so by S13.1, |F_W(x)−W|<ε; also x≠2, so F_W(x)=x+2=4+r and |F_W(x)−4|=r<ε.



S13.3 · impliesBefore

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

After

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

Conditions: none

Rule: contradiction · Uses: S13.2, abs_rules

Leaf basis: contradiction + abs_rules + order_basics

Triangle inequality: |W−4|≤|W−F_W(x)|+|F_W(x)−4|<ε+ε=2ε=|W−4|, giving |W−4|<|W−4|, a contradiction (for example, W=5 gives 2·(1/2)=1=|5−4|, N12). So the assumption W≠4 fails and W=4. S13.1 to S13.3 prove Lemma L_unique_ext.







## Reverse audits


- S14 · sufficient_goal_reduction · S06, S08, S10, S12, S13 — Goal G: the four conclusions of this guide. Each part is proved forwards; the two directions for W=4 come from S12 and S13.
- S13.3 · premise_audit · S13.2, abs_rules, contradiction — The contradiction refutes only W≠4; existence is proved separately in S12.
- S13.2 · premise_audit · S13.1, S11, forall_elim — x≠2 is chosen so that the formula of q applies; r is below both δ and ε.
- S13.1 · premise_audit · continuity_def, exists_elim, abs_rules — W≠4 is needed to make ε>0.
- S13 · premise_audit · L_unique_ext — The lemma uses only the values x+2 at x≠2 and the definition of continuity, not a general theorem on uniqueness of limits.
- S12 · premise_audit · S01, S11, forall_intro — Both kinds of x are checked; ε is arbitrary.
- S11 · inverse_equivalence · frac_rules, distributive — Valid both ways on the domain x≠2; it does not extend to x=2.
- S10 · premise_audit · S01, exists_elim, contradiction — As in S08; one point on the right suffices.
- S09 · premise_audit · G3, mko_continuity, numeric_evaluation — A reading of the defect pair; the independent refutation is S10.
- S08 · premise_audit · S01, exists_elim, contradiction, abs_rules — δ is whatever positive number the assumption supplies; the argument works for every possible δ, so the conclusion does not depend on δ.
- S07 · premise_audit · S03, S04, numeric_evaluation — The defect pair is only a reading of the criterion; the independent refutation is S08.
- S06 · sufficient_goal_reduction · S01, S05, forall_intro — Goal G: f_3 is continuous at 1. Sufficient condition H: for arbitrary ε, δ=ε/5 works; H⇒G by the definition. H is proved forwards from S05, without assuming G.
- S05.3 · premise_audit · numeric_evaluation — With V=4 this case would give 1≤0, which fails; so the lemma is claimed for V=3 only.
- S05.2 · premise_audit · abs_rules, distributive — An equality is in particular a ≤ bound.
- S05.1 · premise_audit · abs_rules, order_basics — Only an upper bound is claimed; comparing 2 with 5 needs |x−1|≥0.
- S05 · premise_audit · L_branch_bound, case_analysis — The three cases are exclusive and cover every x (S02).
- S04 · premise_audit · S03, mko_continuity — The criterion is cited from the MKO; this guide independently verifies V=3 and V=4 in S06 and S08.
- S03 · inverse_equivalence · numeric_evaluation — Exact evaluation; both sides name the same number.
- S02 · premise_audit · G2, function_def, order_basics — Trichotomy of the reals guarantees exactly one case applies.
- S01 · premise_audit · G1, mko_continuity, continuity_def — This step only unfolds the definition.





## Error controls and negative controls

Equal one-sided limits are not enoughOne misconception the MKO lists is ignoring the point value once the one-sided limits agree. Both one-sided limits of f_4 are 3, but f_4(1)=4, and S08 proves directly with ε=1/2 that it is not continuous. Continuity requires 'two-sided limit = centre value'; the centre value is part of the decision.

A centre value matching one side is not enoughg(1)=3 equals the left limit, but the right limit is 4 (S09, S10), so g is not continuous. Both components of the defect pair (L⁻−V, L⁺−V) must be 0.

Removable does not mean no filling is neededAnother misconception is claiming the original quotient is continuous at the centre without filling it. q is undefined at 2 (S11), so continuity at 2 does not even apply; a continuous function on all real numbers requires a value at the missing point, and only W=4 works (S12, S13). An extension filled with another value, for example W=0, is not continuous at 2.


- Both one-sided limits of f_4 are 3, so f_4 is continuous at 1 → reject — f_4(1)=4≠3; x=1−δ/2 gives error 1+δ>1/2 (S08).
- g(1)=3 equals the left limit, so g is continuous at 1 → reject — The right limit is 4; x=1+δ/2 gives error 1+5δ/2>1/2 (S10).
- q(x)=(x²−4)/(x−2) has limit 4 at 2, so q is continuous at 2 → reject — q is undefined at 2; only the extension F_4 with W=4 is continuous at 2.
- Assigning any value at a removable singularity gives a continuous extension, for example F(2)=0 → reject — S13 proves W=4 is forced; with W=0, ε=2 already refutes continuity.
- Checking that f_3(0.9) and f_3(1.1) are close to 3 proves f_3 is continuous at 1 → reject — Finitely many test points are not a proof; the proof is S06's argument for arbitrary ε.





## Result and limitations

f_V has both one-sided limits equal to 3: with V=3 it is continuous at 1 (δ=ε/5); with V=4 it is not (defect pair (−1,−1)). g has one-sided limits 3 and 4, which differ, and its centre value 3 matches only the left side, so it is not continuous (defect pair (0,1)). q=(x²−4)/(x−2) is defined only on ℝ∖{2}; an extension to all real numbers is continuous at 2 exactly when the assigned value is W=4.


- The MKO's criterion 'left limit = right limit = V ⇔ continuous' is cited here and independently checked by ε-δ in the two concrete cases; the general equivalence is not proved in this guide.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 47982f7ca8622e26e45615f6dc3a8550fa228ca562132006c98685246f8606e4
- original source SHA-256: 47982f7ca8622e26e45615f6dc3a8550fa228ca562132006c98685246f8606e4
- 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-continuity-01.json)