Convergence in a metric space: limit and uniqueness for an ultimately constant sequence on a finite metric table

Goal and scope

On the three-point set X={a,b,c} a complete metric table is given: d(a,b)=1, d(a,c)=2, d(b,c)=3/2. The sequence has x_0=a, x_1=c, x_2=a, and it is declared that x_n=b for every n≥3. (1) Check that d is a metric; (2) prove x_n→b from the ε-N definition and find the least valid N for each ε; (3) prove that limits in a metric space are unique, and give direct witnesses that x_n converges neither to a nor to c; (4) using a sequence that agrees with x_n on a finite tail but has a different limit, show that checking a finite tail cannot decide whether the limit is the specified b.

Treats only the finite metric space of G1 and the ultimately constant sequence model of G2 (MKO assumptions a1, a2). The uniqueness-of-limits lemma is proved in full for every metric space, and so is the ultimately-constant lemma. Cauchy sequences, completeness and continuous maps are not treated, and a check of a finite sampled tail is never taken as a proof of convergence. The canonical MKO and its English edition are not changed.

Givens and symbols

• metric_def
• order_basics
• quantifier_negation
• forall_intro
• exists_intro

• G1 — X={a,b,c} with three distinct labels a, b, c. Metric table: d(p,p)=0 for every p∈X; d(a,b)=d(b,a)=1; d(a,c)=d(c,a)=2; d(b,c)=d(c,b)=3/2 (MKO assumption a1: a complete finite metric table).
• G2 — The sequence (x_n)_{n∈ℕ0}: x_0=a, x_1=c, x_2=a, and it is declared that x_n=b for every n≥3 (MKO assumption a2: ultimately constant model with prefix length 3 and tail value b).
• G3 — Comparison sequence (y_n)_{n∈ℕ0}: y_n=x_n for 0≤n≤10, and it is declared that y_n=c for every n≥11.

• X=\{a,b,c\} — the three-point carrier
• d — the complete metric table of G1
• (x_n)_{n\in\mathbb{N}_0} — the ultimately constant sequence: prefix a, c, a and x_n=b for n≥3
• (y_n)_{n\in\mathbb{N}_0} — the comparison sequence equal to x_n for n≤10 and to c for n≥11
• \varepsilon,\ N — tolerance (ε>0) and cutoff index
• (s_n),\ p,\ q,\ M — the generic sequence, candidate limits and prefix length in the lemmas

Rules and sources

• metric_def · prerequisite — Metric: d:X×X→ℝ with d(x,y)≥0 and d(x,y)=0 ⇔ x=y; d(x,y)=d(y,x); triangle inequality d(x,z)≤d(x,y)+d(y,z).
• 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.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• 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).
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• 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.
• modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q.
• 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.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_metric_conv · cited — A sequence x_n in a metric space converges to x if, for every ε>0, there exists N such that all n≥N satisfy d(x_n,x)<ε. Passing a sampled finite tail is insufficient for general convergence; an explicitly ultimately constant infinite sequence can instead provide a complete witness. · mko-metric-convergence
• L_metric_table · lemma — The table d of G1 is a metric on X: d≥0 and d(p,q)=0 ⇔ p=q; d is symmetric; the triangle inequality holds for all 27 ordered triples.
• L_tail_const · lemma — In any metric space, if a sequence (s_n) has s_n=p for every n≥M, then s_n→p, and N=M is a valid cutoff for every ε>0.
• L_limit_unique · lemma — In any metric space, if s_n→p and s_n→q, then p=q.

Main derivation

x_n\to p\ \text{in}\ (X,d)

\forall\varepsilon>0\ \exists N\in\mathbb{N}_0\ \forall n\ge N:\ d(x_n,p)<\varepsilon

d:\ \text{the table of G1}

(X,d)\ \text{is a metric space}

x_0=a,\ x_1=c,\ x_2=a

x_n=b\ \text{for every}\ n\ge 3\ \text{(declared tail)}

x_n=b\ \ (n\ge 3)

x_n\to b

\varepsilon>0

N_{\min}(\varepsilon)=0\ (\varepsilon>\tfrac32),\quad 2\ (1<\varepsilon\le\tfrac32),\quad 3\ (0<\varepsilon\le 1)

x_n\to b\ \land\ x_n\to q

q=b

a\neq b,\ c\neq b

x_n\not\to a,\ \ x_n\not\to c

\neg\,\forall\varepsilon>0\ \exists N\ \forall n\ge N:\ d(x_n,q)<\varepsilon

\exists\varepsilon>0\ \forall N\ \exists n\ge N:\ d(x_n,q)\ge\varepsilon

q=a,\ \varepsilon=1,\ N\ \text{arbitrary}

n=\max(N,3)\ge N:\ d(x_n,a)=d(b,a)=1\ge 1

q=c,\ \varepsilon=\tfrac32,\ N\ \text{arbitrary}

n=\max(N,3)\ge N:\ d(x_n,c)=d(b,c)=\tfrac32\ge\tfrac32

x_n\to b,\ x_n\not\to a,\ x_n\not\to c

\{q\in X\mid x_n\to q\}=\{b\}

y_n=c\ \ (n\ge 11)

y_n\to c\ \land\ y_n\not\to b

x_n=y_n=b\ \ (3\le n\le 10)

\lim x_n=b\neq c=\lim y_n

\text{S02},\ \text{S04},\ \text{S05},\ \text{S11},\ \text{S13}

x_n\to b\ \text{with witness}\ N=3\ \text{for every}\ \varepsilon;\ \text{limit unique}

Substeps and lemmas

d(p,p)=0,\ d(a,b)=1,\ d(a,c)=2,\ d(b,c)=\tfrac32\ \text{(with mirror entries)}

d\ge 0,\ \ (d(p,q)=0\Leftrightarrow p=q),\ \ d(p,q)=d(q,p)

x,y,z\ \text{pairwise distinct}

2\le 1+\tfrac32,\quad 1\le 2+\tfrac32,\quad \tfrac32\le 1+2

x=z\ \lor\ y=x\ \lor\ y=z

d(x,z)\le d(x,y)+d(y,z)

s_n=p\ \text{for all}\ n\ge M

d(s_n,p)=d(p,p)=0\ \text{for all}\ n\ge M

\varepsilon>0\ \text{arbitrary};\ d(s_n,p)=0\ (n\ge M)

\exists N\ (N=M)\ \forall n\ge N:\ d(s_n,p)<\varepsilon

\varepsilon\ \text{arbitrary}:\ \exists N\ \forall n\ge N:\ d(s_n,p)<\varepsilon

\forall\varepsilon>0\ \exists N\ \forall n\ge N:\ d(s_n,p)<\varepsilon,\ \text{i.e.}\ s_n\to p

\varepsilon>\tfrac32

N=0\ \text{valid, hence}\ N_{\min}=0

1<\varepsilon\le\tfrac32

N\in\{0,1\}\ \text{invalid},\ N=2\ \text{valid, hence}\ N_{\min}=2

0<\varepsilon\le 1

N\le 2\ \text{invalid},\ N=3\ \text{valid, hence}\ N_{\min}=3

s_n\to p,\ s_n\to q,\ \varepsilon>0

\exists N:\ d(s_N,p)<\tfrac{\varepsilon}{2}\ \land\ d(s_N,q)<\tfrac{\varepsilon}{2}

d(s_N,p)<\tfrac{\varepsilon}{2},\ d(s_N,q)<\tfrac{\varepsilon}{2}

d(p,q)\le d(p,s_N)+d(s_N,q)<\tfrac{\varepsilon}{2}+\tfrac{\varepsilon}{2}=\varepsilon

\forall\varepsilon>0:\ d(p,q)<\varepsilon

d(p,q)=0

d(p,q)=0

p=q

Reverse audits

• S14 · premise_audit · S02, S04, S05, S11, S13 — This only conjoins conclusions already proved; there is no new inference.
• S13 · premise_audit · S04, S12, L_tail_const — The conclusion is only that finite data do not decide the limit; it does not deny x_n→b, because the convergence of x comes from the declaration of S03 for all n≥3, not from the finite tail.
• S12 · premise_audit · G3, L_tail_const, L_limit_unique — Both lemmas were proved for any metric space; this step only instantiates them.
• S11 · premise_audit · S04, S09, S10, G1 — Saying 'exactly' needs the complete list of X (G1); excluding only some points would not suffice.
• S10 · premise_audit · S08, S03, exists_intro — The same premises as S09; only the target point and ε change.
• S09 · premise_audit · S08, S03, exists_intro, forall_intro — One ε is enough; an n must be found for every N, and the construction max(N,3) works for arbitrary N. The prefix terms x_0=a and x_2=a do not help the opposite conclusion at all.
• S08 · inverse_equivalence · quantifier_negation, order_basics — Quantifier negation holds in both directions; trichotomy of the reals makes ¬(d<ε) equivalent to d≥ε.
• S07 · premise_audit · S06, contrapositive — The contrapositive is equivalent to the original statement, so this is a valid one-way inference; S08 to S10 give direct witnesses as a cross-check.
• S06.4 · premise_audit · metric_def — This uses the ⇒ direction of separation; for a pseudometric (allowing d(p,q)=0 with p≠q) limits need not be unique.
• S06.3 · premise_audit · S06.2, contradiction, order_basics — The key point is that S06.2 holds for every ε>0, so ε=d(p,q) may be used; if it held only for some ε, this choice would not be allowed.
• S06.2 · premise_audit · metric_def, order_basics, forall_intro — Uses the triangle inequality, symmetry and the addition of inequalities; only an upper bound is obtained, no equality is claimed.
• S06.1 · premise_audit · forall_elim, exists_elim, order_basics — Instantiation needs ε/2>0; taking the max puts one index in both tails at once. N_1 and N_2 are fresh names from ∃-elimination, and the final conclusion p=q does not mention them.
• S06 · premise_audit · S02, S04, L_limit_unique — Requires d to be a genuine metric (S02); if the table violated the triangle inequality, S06.2 could not be taken.
• S05.3 · premise_audit · S05, S03, order_basics — Rejecting N≤2 uses the term n=2; accepting N=3 uses the declaration of S03 for all n≥3.
• S05.2 · premise_audit · S05, order_basics — Rejecting an N needs one bad index (n=1); accepting N=2 needs every tail term, which the prefix values and the declaration of S03 supply.
• S05.1 · premise_audit · S05, order_basics — Uses the complete list of distance values (three prefix terms plus the constant tail of S03) and transitivity d≤3/2<ε.
• S05 · premise_audit · S03, case_analysis — The intervals (3/2,∞), (1,3/2] and (0,1] are pairwise disjoint with union (0,∞), so the cases are exhaustive.
• S04.3 · premise_audit · S04.2, forall_intro, S01 — The generalization needs ε to be arbitrary; no particular ε was chosen in the proof.
• S04.2 · premise_audit · S04.1, order_basics — ε>0 is needed for 0<ε; if ε=0 were allowed, the strict inequality 0<0 would fail, and the definition does not ask for it.
• S04.1 · premise_audit · eq_replace, metric_def — This is claimed only for n≥M; the terms with n<M are unrestricted and do not affect the conclusion.
• S04 · premise_audit · S03, L_tail_const — The only premises are 'x_n=b for every n≥3' and d(b,b)=0. The converse (convergence implies ultimately constant) is not needed here; it does hold in finite metric spaces, but fails in general metric spaces such as ℝ (the separately positive-indexed sequence 1/n, n≥1, tends to 0 without being ultimately constant).
• S03 · premise_audit · G2, def_intro — This step only records the declaration of G2; without a declaration for all n≥3, no finite list could determine the behaviour of the tail.
• S02.3 · premise_audit · S02.1, case_analysis — The cases must cover every triple with a repeated point: if the three points are not all distinct, then x=y, y=z or x=z, which are exactly these cases.
• S02.2 · premise_audit · S02.1, numeric_evaluation — Each inequality is recomputed independently in N1, N2 and N3; the reduction to 3 inequalities uses the symmetry from S02.1.
• S02.1 · premise_audit · G1, metric_def, numeric_evaluation — Only the enumeration of all 9 cells supports these three axioms; leaving out a cell would make it a partial check.
• S02 · premise_audit · L_metric_table, metric_def — Only this table is claimed to be a metric, not any other table. Here the triangle inequality amounts to finitely many inequalities, and the conclusion follows only after all of them are enumerated.
• S01 · premise_audit · mko_metric_conv — This step only unfolds the definition and produces no new fact; the definition presupposes that (X,d) is a metric space, which S02 checks.

Error controls and negative controls

A finite tail is not a proof of convergence

The misconception named by the MKO is to assert convergence because a long but finite tail looks close. The sequence y_n of S13 equals x_n for n=3 to 10 (all equal to b), yet it converges to c. x_n→b holds because G2 declares x_n=b for every n≥3; that is a rule covering infinitely many terms, not the result of a finite check.

Strict inequality and quantifier order

The definition uses d(x_n,x)<ε, a strict inequality. In S09, d(x_n,a)=1 does not satisfy < for ε=1, so ε=1 already excludes a; with ≤ by mistake this particular witness would fail (although ε=1/2 would still exclude a). The quantifier order allows N to depend on ε but does not require dependence: N=3 works for every ε>0 here, while S05 shows that the least valid N changes from 0 to 2 to 3 as ε shrinks.

Check the metric table first

The uniqueness proof S06.2 uses the triangle inequality. If the table were miswritten with d(a,c)=3 (everything else unchanged), then d(a,c)=3>d(a,b)+d(b,c)=5/2, the triangle inequality fails, the table is not a metric, and the argument of S06 cannot be used. So S02 must be completed before any convergence reasoning.

• x_3 to x_10 all equal b, so every sequence with these terms converges to b → reject — y_n has exactly these terms but converges to c (S12, S13).
• Since x_0=a and x_2=a, x_n→a → reject — Convergence depends only on the tail: with ε=1, for every N the index n=max(N,3) gives d(x_n,a)=1≥1 (S09).
• For n≥3, d(x_n,a)=1≤1, so taking ε=1 shows that x_n converges to a → reject — The definition requires every ε>0 and a strict <; at ε=1 already 1<1 fails, and at ε=1/2 it fails as well.
• In some metric space a sequence can converge to both b and c → reject — L_limit_unique holds in every metric space: the distance between two limits is below every ε>0, hence 0, and separation gives b=c; here d(b,c)=3/2>0.

Result and limitations

The table of G1 is a metric; the sequence x_n (prefix a, c, a, then constantly b for n≥3) converges to b, with N=3 valid for every ε>0 and least valid N equal to 0, 2, 3 for ε>3/2, 1<ε≤3/2, 0<ε≤1 respectively; limits in a metric space are unique, and x_n converges neither to a (witness ε=1) nor to c (witness ε=3/2). The sequence y_n, which agrees with x_n on a finite tail, converges to c instead, both sequences converge but have different limits, so a finite tail check cannot decide whether the limit is the specified b. This pair by itself does not distinguish existence from nonexistence of a limit.

• This guide does not treat Cauchy sequences, completeness or continuous maps (the MKO's formal next).
• The remark in the audit of S04 that convergence implies ultimately constant in a finite metric space (provable by taking ε to be the least positive distance) is only a note; the argument of this guide does not depend on it.
• The least valid N of S05 holds only for this sequence and this table.

Verification and source binding

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

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

Same-source full JSON (formulas, ASTs, controls and revision log)