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

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

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

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

s,t\ge 0

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

m,n\ge N\ge 1

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

m,n\ge N\ge 1

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

\varepsilon>0\ \text{arbitrary}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Substeps and lemmas

s\ge t\ge 0

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

t>s\ge 0

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

m\ge N>0

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

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

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

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

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

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

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

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 Cauchy

The 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 ones

Cauchy 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 limit

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