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

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

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

Substeps and lemmas

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

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 enough

One 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 enough

g(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 needed

Another 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)