# Cauchy sequence: a complete certificate for the reciprocal sequence, a space in which it has no limit, an alternating counterexample and an ultimately constant model

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

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



## Goal and scope

(1) Prove that x_n=1/n (n≥1) is a Cauchy sequence in (ℝ, |s−t|): for every ε>0 give N such that |1/m−1/n|<ε for all m,n≥N. (2) Prove that the same sequence is still Cauchy in X=(0,1] with the restricted metric, but has no limit in X. (3) Prove that y_n=(−1)^n is not Cauchy. (4) Prove that the ultimately constant sequence z (z₁=0, z₂=7, z_n=5 for n≥3) is Cauchy. Also explain why a finite tail cannot prove the Cauchy property.

Stays inside the MKO's slice: complete certificates only for an explicit ultimately constant model, reciprocal-sequence bounds and one exact counterexample family (the alternating sequence). The metric is |s−t| on ℝ and its restriction to (0,1]. The general theory of complete metric spaces and Banach spaces is not treated; finitely listed tails serve only as bounded audits; the canonical MKO and its English edition are not changed.





## Givens and symbols


- metric_def
- seq_limit_def
- archimedean
- abs_rules
- order_basics
- quantifier_negation


- G1 — (ℝ,d) with d(s,t)=|s−t|; X=(0,1]={t ∣ 0<t≤1}, with the same formula d(s,t)=|s−t| restricted to X.
- G2 — x_n=1/n for n≥1.
- G3 — y_n=(−1)^n for n≥1.
- G4 — z₁=0, z₂=7, and z_n=5 for every n≥3.


- d(s,t)=|s-t| — the standard metric on ℝ
- X=(0,1] — the subspace with the restricted metric
- x_n=\tfrac1n — the reciprocal sequence
- y_n=(-1)^n — the alternating sequence
- z_n — the ultimately constant sequence
- \varepsilon,\ N — the tolerance and the start of the tail





## 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).
- seq_limit_def · prerequisite — Limit of a sequence: a_n→L means that for every ε>0 there is N such that |a_n−L|<ε for all n≥N.
- archimedean · prerequisite — Archimedean property: for every real x there is a natural number n>x; hence for every ε>0 there is n with 1/n<ε.
- 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.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬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.
- 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_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.
- 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.
- 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.
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
- neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- mko_cauchy · cited — A sequence (x_n) is Cauchy if for every ε>0 there exists N such that all m,n≥N satisfy d(x_m,x_n)<ε. The definition does not first assume that a limit exists or belongs to the space. A finitely listed tail supplies only a bounded audit, not a proof of the general Cauchy property. · mko-cauchy-sequence
- max_two · prerequisite — Maximum of two numbers: max(s,t) is the larger of s and t; max(s,t)≥s and max(s,t)≥t; if s≤K and t≤K, then max(s,t)≤K.
- subspace_metric · prerequisite — Subspace metric: for X⊆ℝ, d(s,t)=|s−t| restricted to X is still a metric. A sequence in X converges in X to L when L∈X and for every ε>0 there is N with |x_n−L|<ε for n≥N.
- L_absmax · lemma — If s≥0 and t≥0, then |s−t|≤max(s,t).
- L_recip · lemma — For reals m≥N>0: 0<1/m≤1/N; and if m>N, then 1/m<1/N.





## Main derivation

S01 · equivalentBefore

(x_n)\ \text{Cauchy in}\ (\mathbb{R},d)

After

\forall\varepsilon>0\ \exists N\ \forall m,n\ge N:\ \left|\tfrac1m-\tfrac1n\right|<\varepsilon

Conditions: none

Rule: mko_cauchy · Uses: G1, G2, mko_cauchy

Leaf basis: mko_cauchy + def_unfold

Unfold the MKO's definition: what is compared is the distance between any two terms of the tail, and no limit appears in the definition. N may depend on ε but not on m or n.



S02 · impliesBefore

s,t\ge 0

After

|s-t|\le\max(s,t)

Conditions: s\ge 0; t\ge 0

Rule: L_absmax · Uses: L_absmax

Leaf basis: L_absmax

Lemma L_absmax: the absolute difference of two nonnegative numbers is at most the larger of them. The proof in S02.1 and S02.2 splits into the cases s≥t and s<t. It will be used with s=1/m and t=1/n.



S03 · impliesBefore

m,n\ge N\ge 1

After

0<\tfrac1m\le\tfrac1N,\ 0<\tfrac1n\le\tfrac1N

Conditions: N\ge 1

Rule: L_recip · Uses: L_recip

Leaf basis: L_recip

By Lemma L_recip (proved in S03.1), m≥N>0 gives 0<1/m≤1/N, and likewise for n. Every term of the tail lies in (0,1/N].



S04 · impliesBefore

m,n\ge N\ge 1

After

\left|\tfrac1m-\tfrac1n\right|\le\max\left(\tfrac1m,\tfrac1n\right)\le\tfrac1N

Conditions: N\ge 1

Rule: max_two · Uses: S02, S03, max_two

Leaf basis: L_absmax + max_two + order_basics

L_absmax (s=1/m≥0, t=1/n≥0) gives the first inequality; by S03 both are ≤1/N, so their maximum is ≤1/N. This bound is uniform over all m, n in the tail, whatever their relative size.



S05 · impliesBefore

\varepsilon>0\ \text{arbitrary}

After

\exists N\in\mathbb{N},\ N\ge 1:\ \tfrac1N<\varepsilon

Conditions: \varepsilon>0

Rule: archimedean · Uses: archimedean

Leaf basis: archimedean

Take an arbitrary ε>0, with no other assumption. By the Archimedean property there is a natural number N with 1/N<ε; N≥1 can be taken. For example, with ε=1/10, N=11 works.



S06 · impliesBefore

m,n\ge N,\ \tfrac1N<\varepsilon

After

\left|\tfrac1m-\tfrac1n\right|\le\tfrac1N<\varepsilon

Conditions: none

Rule: order_basics · Uses: S04, S05, order_basics

Leaf basis: order_basics + forall_intro

For the N chosen in S05 and any m,n≥N, S04 gives |1/m−1/n|≤1/N, and 1/N<ε with transitivity of order gives |1/m−1/n|<ε.



S07 · impliesBefore

\text{for arbitrary } \varepsilon>0:\ N\ \text{found with S06}

After

(x_n)=(\tfrac1n)\ \text{is Cauchy in}\ (\mathbb{R},d)

Conditions: none

Rule: forall_intro · Uses: S01, S06, forall_intro, exists_intro

Leaf basis: forall_intro + exists_intro

For each ε an N was found (∃-introduction), and ε was arbitrary (∀-introduction); by S01, (1/n) is Cauchy in (ℝ,d). This is a complete certificate covering every ε (the reciprocal-sequence bound allowed by MKO assumption a2).



S08 · impliesBefore

x_n\in X?\ \text{and}\ d_X(x_m,x_n)

After

x_n\in(0,1],\ d_X(x_m,x_n)=\left|\tfrac1m-\tfrac1n\right|;\ (x_n)\ \text{Cauchy in}\ X

Conditions: none

Rule: subspace_metric · Uses: G1, S03, S07, subspace_metric

Leaf basis: subspace_metric + L_recip

By L_recip with N=1, 0<1/n≤1, so every term lies in X. The distance on X is the same formula, so every inequality of S04 to S07 is unchanged and (x_n) is Cauchy in X as well. The Cauchy property depends only on distances between terms.



S09 · impliesBefore

\text{suppose } L\in X\ \text{and}\ x_n\to L\ \text{in}\ X

After

\text{contradiction; no } L\in X\ \text{is a limit of}\ (x_n)

Conditions: none

Rule: contradiction · Uses: S08, subspace_metric, contradiction

Leaf basis: contradiction + seq_limit_def

By contradiction: suppose some L∈X (so L>0) is a limit. S09.1 takes N₁ for ε=L/2; S09.2 uses the Archimedean property to find n≥N₁ with 1/n<L/2; S09.3 shows that then |1/n−L|>L/2, contradicting S09.1. So (x_n) has no limit in X.



S10 · impliesBefore

(x_n)\ \text{Cauchy in}\ X,\ \text{no limit in}\ X

After

\text{Cauchy does not presuppose a limit in the space}

Conditions: none

Rule: and_intro_elim · Uses: S08, S09, mko_cauchy

Leaf basis: and_intro_elim + mko_cauchy

In X=(0,1], (1/n) is Cauchy (S08) yet has no limit (S09). This is exactly the MKO's point: the definition does not first assume that a limit exists or belongs to the space. X is not a complete metric space, but this guide does not develop the theory of completeness.



S11 · impliesBefore

y_{n+1}=(-1)^{n+1}=-y_n

After

|y_n-y_{n+1}|=|2y_n|=2|y_n|=2\ \text{for every } n\ge 1

Conditions: none

Rule: abs_rules · Uses: G3, abs_rules, power_laws

Leaf basis: power_laws + abs_rules + neg_mul

(−1)^(n+1)=(−1)^n·(−1)=−y_n, so y_n−y_(n+1)=2y_n, and |y_n|=|±1|=1, giving |y_n−y_(n+1)|=2. This holds for every n, not just for some listed terms.



S12 · equivalentBefore

\neg\,(y_n)\ \text{Cauchy}

After

\exists\varepsilon>0\ \forall N\ \exists m,n\ge N:\ |y_m-y_n|\ge\varepsilon

Conditions: none

Rule: quantifier_negation · Uses: mko_cauchy, quantifier_negation

Leaf basis: quantifier_negation + order_basics

Negating the statement ∀ε∃N∀m,n flips each quantifier in turn and replaces <ε by ≥ε. So to refute the Cauchy property one ε is enough, such that beyond every N there are two terms at distance at least ε.



S13 · impliesBefore

\varepsilon=1,\ N\ \text{arbitrary},\ m=N,\ n=N+1

After

|y_N-y_{N+1}|=2\ge 1;\ (y_n)\ \text{is not Cauchy}

Conditions: none

Rule: exists_intro · Uses: S11, S12, exists_intro

Leaf basis: exists_intro + forall_intro + order_basics

Take ε=1. For any N take the adjacent m=N and n=N+1 (both ≥N); by S11 their distance is 2≥1. By the equivalence of S12, (y_n) is not Cauchy. This is the MKO's alternating counterexample family: for every N there is an adjacent counterexample.



S14 · impliesBefore

\varepsilon>0\ \text{arbitrary},\ N=3

After

m,n\ge 3\Rightarrow|z_m-z_n|=|5-5|=0<\varepsilon;\ (z_n)\ \text{Cauchy}

Conditions: \varepsilon>0

Rule: forall_intro · Uses: G4, mko_cauchy, forall_intro

Leaf basis: forall_intro + exists_intro + numeric_evaluation

Ultimately constant model: for any ε>0 take N=3, independent of ε. For m,n≥3, z_m=z_n=5 and the distance is 0<ε. Since ε is arbitrary, (z_n) is Cauchy. The first two terms 0 and 7 do not affect the conclusion, because the definition looks only at the tail (MKO para1).







## Substeps and lemmas

S02.1 · impliesBefore

s\ge t\ge 0

After

|s-t|=s-t\le s=\max(s,t)

Conditions: s\ge t; t\ge 0

Rule: abs_rules · Uses: abs_rules, max_two, order_basics

Leaf basis: abs_rules + max_two + order_basics

When s≥t, s−t≥0, so |s−t|=s−t; since t≥0, s−t≤s; and when s≥t, max(s,t)=s.



S02.2 · impliesBefore

t>s\ge 0

After

|s-t|=t-s\le t=\max(s,t)

Conditions: t>s; s\ge 0

Rule: case_analysis · Uses: S02.1, abs_rules, max_two, case_analysis

Leaf basis: abs_rules + max_two + case_analysis

When t>s, s−t<0 and |s−t|=t−s; since s≥0, t−s≤t=max(s,t). The cases s≥t and t>s cover everything, so S02.1 and S02.2 together prove L_absmax.



S03.1 · impliesBefore

m\ge N>0

After

\tfrac1N=m\cdot\tfrac{1}{mN}\ge N\cdot\tfrac{1}{mN}=\tfrac1m>0

Conditions: N>0

Rule: order_basics · Uses: order_basics, mul_inverse_nonzero, frac_rules

Leaf basis: order_basics + mul_inverse_nonzero + frac_rules

m≥N>0 gives m>0 and mN>0, so 1/(mN)>0. Multiplying m≥N by the positive number 1/(mN) keeps the direction: 1/N≥1/m; if m>N it is strict: 1/N>1/m. Also 1/m>0, since the reciprocal of a positive number is positive. This proves L_recip.



S09.1 · impliesBefore

x_n\to L\in X,\ \varepsilon=\tfrac L2>0

After

\exists N_1\ \forall n\ge N_1:\ \left|\tfrac1n-L\right|<\tfrac L2

Conditions: L>0

Rule: seq_limit_def · Uses: subspace_metric, seq_limit_def

Leaf basis: seq_limit_def + forall_elim

L∈X means L>0, so ε=L/2>0 is a legitimate tolerance; the definition of limit gives N₁.



S09.2 · impliesBefore

n_0>\tfrac2L\ \text{(Archimedean)},\ n=\max(n_0,N_1)

After

n\ge N_1,\ \tfrac1n\le\tfrac1{n_0}<\tfrac L2

Conditions: L>0

Rule: archimedean · Uses: S09.1, archimedean, L_recip, max_two

Leaf basis: archimedean + L_recip + max_two

By the Archimedean property take a natural number n₀>2/L>0. Let n=max(n₀,N₁); then n≥N₁ and n≥n₀. By L_recip, 1/n≤1/n₀, and since n₀>2/L, 1/n₀<1/(2/L)=L/2.



S09.3 · impliesBefore

\tfrac1n<\tfrac L2,\ n\ge N_1

After

\left|\tfrac1n-L\right|\ge L-\tfrac1n>L-\tfrac L2=\tfrac L2

Conditions: none

Rule: abs_rules · Uses: S09.1, S09.2, abs_rules

Leaf basis: abs_rules + order_basics + contradiction

|w|≥−w holds for every real w; with w=1/n−L this gives |1/n−L|≥L−1/n. From 1/n<L/2, L−1/n>L/2. So |1/n−L|>L/2, yet n≥N₁ and S09.1 requires |1/n−L|<L/2, a contradiction.







## Reverse audits


- S14 · premise_audit · G4, mko_cauchy, forall_intro — It needs the constant value 5 for all n≥3 (stated in G4), not only for some listed terms.
- S13 · premise_audit · S11, S12, exists_intro, forall_intro — It needs a witness for every N; S11 holds for all n, so a witness exists for every N.
- S12 · inverse_equivalence · quantifier_negation, order_basics — Quantifier negation and ¬(d<ε) ⇔ d≥ε are both two-way.
- S11 · premise_audit · abs_rules, power_laws — It uses the exponent laws and |uv|=|u||v|; it holds for all n.
- S10 · premise_audit · S08, S09, and_intro_elim — It only conjoins two proved conclusions; the sentence on completeness is a remark.
- S09.3 · premise_audit · S09.1, S09.2, abs_rules, order_basics — The same n satisfies two contradictory inequalities; the contradiction comes from the assumption that some L∈X is a limit.
- S09.2 · premise_audit · archimedean, L_recip, max_two — The same n satisfies both n≥N₁ and 1/n<L/2, which is the purpose of taking the maximum.
- S09.1 · premise_audit · seq_limit_def, subspace_metric — It needs L>0; this is exactly where 0∉X matters.
- S09 · premise_audit · subspace_metric, contradiction — L is an arbitrary point of X, so every possible limit is ruled out; the claim is only that there is no limit in X (in ℝ the limit 0 exists, but 0∉X).
- S08 · premise_audit · S03, S07, subspace_metric — It needs all terms in X and the same metric; no limit is involved.
- S07 · premise_audit · S01, S06, forall_intro, exists_intro — It needs the arbitrariness of ε and the existence of N; the argument uses no limit at all.
- S06 · premise_audit · S04, S05, order_basics — Chaining ≤ and < gives <; no converse is claimed.
- S05 · premise_audit · archimedean — N depends only on ε, which is exactly what the position of ∃N in the Cauchy definition allows.
- S04 · premise_audit · S02, S03, max_two — It needs both terms nonnegative and both ≤1/N; equality is not claimed.
- S03.1 · premise_audit · order_basics, mul_inverse_nonzero, frac_rules — It needs N>0 so that the reciprocals exist and the multiplier is positive; L_recip itself is not used.
- S03 · premise_audit · L_recip — It needs N>0; no converse is claimed.
- S02.2 · premise_audit · abs_rules, max_two, case_analysis — It uses s≥0; the two cases cover all pairs of reals; L_absmax itself is not used.
- S02.1 · premise_audit · abs_rules, max_two, order_basics — It uses t≥0; L_absmax itself is not used.
- S02 · premise_audit · L_absmax — It needs s and t nonnegative; it fails for negatives, for example |(−1)−1|=2>1=max(−1,1).
- S01 · inverse_equivalence · mko_cauchy, def_unfold — Unfolding and folding the definition undo each other, so the step holds both ways.





## Error controls and negative controls

A close finite tail does not prove CauchyThe mistake named by the MKO is to call the whole infinite sequence Cauchy because a long finite tail is close together. For the harmonic partial sums H_n=Σ_{k=1}^{n} 1/k the adjacent differences 1/(n+1) keep shrinking, and any listed finite tail may look close; but for every N, H_{2N}−H_N=Σ_{k=N+1}^{2N} 1/k≥N·1/(2N)=1/2 (each term 1/k≥1/(2N)), so the Cauchy condition fails for ε=1/2.

Compare any two terms of the tail, not only adjacent onesCauchy requires all m,n≥N, not only n and n+1. The harmonic partial sums have adjacent differences tending to 0 yet are not Cauchy. On the other hand, adjacent terms suffice to refute (−1)^n (S13), because a refutation needs only one pair of witnesses.

Do not presuppose a limitS01 to S07 never use a limit. If 'Cauchy' is misread as 'close to some candidate limit', then in X=(0,1] there is no candidate (S09), and yet the sequence is still Cauchy (S08).


- The adjacent differences 1/(n+1) of the harmonic partial sums H_n tend to 0, so (H_n) is Cauchy → reject — For every N, H_{2N}−H_N≥1/2.
- (y_n)=((−1)^n) takes only the two values −1 and 1, so it is Cauchy → reject — With ε=1, |y_N−y_(N+1)|=2≥1 for every N.
- (1/n) is Cauchy in X=(0,1], so it converges in X → reject — S09: no point of X is its limit.
- Listing the first 1000 terms of 1/n and checking their mutual distances proves that (1/n) is Cauchy → reject — A finite tail is only a bounded audit (MKO assumption a1); the proof is the argument of S02 to S07 for every ε.





## Result and limitations

(1/n) is Cauchy in (ℝ,|·|): for every ε>0 take N with 1/N<ε; then |1/m−1/n|≤1/N<ε for all m,n≥N. It is still Cauchy in X=(0,1], yet has no limit in X. (−1)^n is not Cauchy: with ε=1, for every N two adjacent terms are 2 apart. The ultimately constant sequence z is Cauchy, with N=3 working for every ε.


- N3 and N5 are finite-range checks (m, n from 1 to 30; n from 1 to 40); they support only those points and do not prove L_absmax or the general claim of S11, which come from the arguments of S02.1, S02.2 and S11.
- The harmonic partial sums in the error controls are not among the certificate types listed by the MKO and serve only as a counterexample illustration; their lower-bound argument is given in full in the error control, and N10, N11 check only N=2 and N=3.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 3cf4cca5b06ba03d3f526ddbf2d5e9556d77fa989091a6210c0ad46c7169d2a5
- original source SHA-256: 3cf4cca5b06ba03d3f526ddbf2d5e9556d77fa989091a6210c0ad46c7169d2a5
- 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-cauchy-sequence-01.json)