Sequences: fixing the general term from an initial condition and a recurrence, and the pitfalls of indexing and finite prefixes

Goal and scope

Let the real sequence a:ℕ→ℝ (with 0∈ℕ) satisfy a₀=5 and a_{n+1}=a_n+3. (1) Prove that exactly one such sequence exists and that a_n=5+3n; (2) compute a₀ to a₄ and a₁₀, explaining that a₀ is the initial term and a₁₀ is the 11th value when counting from 1; (3) write down the finite sequence of length L=4 and its index set; (4) show that the prefix 5, 8, 11 does not determine the sequence.

Inside the MKO's scope: a real sequence is a function ℕ→ℝ with 0∈ℕ (assumption a1); a finite sequence states its length L and index set, and a recurrence comes with its initial condition (assumption a2), in the MKO's form a₀=u, a_{n+1}=a_n+d with u=5 and d=3. Existence is proved by exhibiting the general term, so no general recursion theorem is needed. It does not treat limits, monotonicity or series, and does not change the canonical MKO or its English edition.

Givens and symbols

• nat_induction
• function_def
• distributive
• add_assoc
• eq_replace
• numeric_evaluation

• G1 — ℕ includes 0; a real sequence is a function a:ℕ→ℝ, a_n denotes a(n), and a₀ is called the initial term (MKO assumption a1).
• G2 — Recurrence with initial condition: a₀=5 and a_{n+1}=a_n+3 for every n∈ℕ.
• G3 — Finite sequence: the length L is a nonnegative integer, the index set is {n∈ℕ ∣ n<L}, and only these n are permitted (MKO assumption a2).

• a_n — the value a(n) of the sequence a at index n
• s_n — the candidate general term 5+3n
• c_n — another sequence with the same prefix as a
• L — the length of a finite sequence
• \mathbb{N} — the natural numbers, including 0

Rules and sources

• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• 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.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• add_zero · prerequisite — Additive identity: u+0=u.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• 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.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• mko_seq_def · cited — Under the convention that ℕ includes 0, a real sequence is a function a:ℕ→ℝ whose nth term is written a(n) or a_n. A finite sequence instead states a length L and the index set (the integers from 0 to L−1). · mko-sequence
• L_unique · lemma — If a sequence a:ℕ→ℝ satisfies a₀=5 and a_{n+1}=a_n+3 for every n, then a_n=5+3n for every n∈ℕ.

Main derivation

(a_n)

a:\mathbb{N}\to\mathbb{R},\ a_0=5,\ a_{n+1}=a_n+3

n\in\mathbb{N}

s:\mathbb{N}\to\mathbb{R},\ s_n=5+3n

s_0

s_0=5+3\cdot 0=5

s_{n+1}=5+3(n+1)

s_{n+1}=(5+3n)+3=s_n+3

s_0=5,\ s_{n+1}=s_n+3

\exists\ a:\mathbb{N}\to\mathbb{R}\ \text{with}\ a_0=5,\ a_{n+1}=a_n+3

a_0=5,\ a_{n+1}=a_n+3

a_n=5+3n\ \text{for every}\ n\in\mathbb{N},\ \text{so}\ a=s

a_n=5+3n

a_0=5,\ a_1=8,\ a_2=11,\ a_3=14,\ a_4=17,\ a_{10}=35

a_{10}=35

a_{10}\ \text{is the 11th value};\ b_k=a_{k-1}\ (k\geq 1)\ \text{gives}\ b_{10}=a_9=32

L=4

(a_0,a_1,a_2,a_3)=(5,8,11,14),\ \ \text{indices}\ \{0,1,2,3\}

c_n=5+3n+n(n-1)(n-2)

c_0=5,\ c_1=8,\ c_2=11

c_3

c_3=5+9+3\cdot 2\cdot 1=20\neq 14=a_3,\ \text{so}\ c\neq a

c_3-c_2

c_3-c_2=20-11=9\neq 3

S05\ \text{to}\ S09,\ S11

a_n=5+3n\ \text{unique};\ a_{10}=35;\ (5,8,11,14)\ \text{on}\ \{0,1,2,3\};\ \text{prefix not determining}

Substeps and lemmas

a_0=5

a_0=s_0

a_n=s_n

a_{n+1}=a_n+3=s_n+3=s_{n+1}

Reverse audits

• S13 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S11, and_intro_elim — Goal G: (1) to (4). Sufficient condition H: the listed steps hold; H⇒G by conjunction introduction. H is proved forwards from the definitions, induction and exact computation; G is never used as a premise.
• S12 · premise_audit · S06, S11, contrapositive — By the contrapositive of S06, c≠a implies that c does not satisfy G2; here the failing index n=2 is also found directly.
• S11 · premise_audit · S10, function_def, numeric_evaluation — One differing index suffices to show the sequences differ (N10, N11).
• S10 · premise_audit · mul_zero, S07 — c_n=a_n is claimed only for n=0, 1, 2; N9 is a finite check at these three points and covers exactly what this step claims.
• S09 · premise_audit · G3, mko_seq_def — The index set is fixed by L, from 0 to L−1, with L elements; common slips are writing 1 to 4 or 0 to 4.
• S08 · premise_audit · S07, G1, def_unfold — Both conventions describe the same list of numbers with labels shifted by 1; this guide uses the MKO's convention of starting at 0.
• S07 · premise_audit · S06, forall_elim, numeric_evaluation — Exact integer computation, independently recomputable (N3 to N5).
• S06.2 · premise_audit · S04, eq_replace, nat_induction — Only the induction hypothesis for the same n is used; no converse is claimed.
• S06.1 · premise_audit · S03, eq_refl_symm_trans — The base case uses only the initial condition; it cannot be derived from the recurrence alone.
• S06 · premise_audit · L_unique, function_def, S05 — Uniqueness needs both the initial condition and the recurrence; with the recurrence alone, a₀=0 would also fit and give a different sequence.
• S05 · premise_audit · S03, S04, exists_intro — This is existence only; that there is just one is proved in S06.
• S04 · inverse_equivalence · distributive, add_assoc — Only identities valid for all n are used, so the step is two-way; N2 checks it as a degree-one polynomial identity.
• S03 · inverse_equivalence · mul_zero, add_zero, eq_replace — Both sides are the same number, so the equation holds both ways (N1).
• S02 · premise_audit · def_intro, function_def — This step only introduces a name; whether s meets the conditions is checked in S03 and S04.
• S01 · premise_audit · G1, G2, mko_seq_def — This step only states the definition and the conditions and derives no new fact.

Error controls and negative controls

State whether indexing starts at 0 or at 1

The first mistake named by the MKO is confusing indexing from 0 with indexing from 1. Here a₀=5 is the initial term and a₁₀=35; with 1-based labels b_k=a_{k−1}, the 'tenth term' is b₁₀=32. The same list of numbers gives different 'tenth terms' under the two labelings, so the convention must be stated first.

A finite prefix does not determine a sequence

The second mistake named by the MKO is claiming that a prefix pins down a unique sequence. After 5, 8, 11, a continues with 14 and c with 20; in fact any finite prefix can be followed by any values. What determines a sequence is an explicit rule (a general term, or a recurrence with initial conditions), and S06 proves uniqueness from exactly such a rule.

A finite sequence has indices only up to L−1

The finite sequence of length L=4 has the 4 indices 0, 1, 2, 3. Writing 1 to 4 loses a₀ and adds a non-existent a₄; writing 0 to 4 gives 5 indices, so length 5. a₄=17 belongs to the infinite sequence, not to this finite one.

• From 5, 8, 11 the next term must be 14 → reject — c_n=5+3n+n(n−1)(n−2) has the same prefix but c₃=20.
• Under 1-based labels the tenth term is 35 → reject — b₁₀=a₉=32; 35 is a₁₀, the 11th value.
• The finite sequence (5,8,11,14) of length 4 has a term a₄=17 → reject — Its indices are only 0, 1, 2, 3; 4<4 fails.
• The finite sequences (5,8) and (8,5) are equal because both have value set {5,8} → reject — A sequence is a function; the values at index 0 are 5≠8. The order of indices is part of the data.
• c also satisfies c₀=5 and c_{n+1}=c_n+3 → reject — c₃−c₂=9≠3.

Result and limitations

Exactly one sequence satisfies a₀=5 and a_{n+1}=a_n+3, namely a_n=5+3n; a₀ to a₄ are 5, 8, 11, 14, 17 and a₁₀=35 (the 11th value counting from 1; under 1-based labels the 'tenth term' is 32). The finite sequence of length 4 is (5,8,11,14) with indices {0,1,2,3}. The prefix 5, 8, 11 is also the prefix of c_n=5+3n+n(n−1)(n−2), but c₃=20≠14, so a prefix does not determine the sequence.

• N9 is a finite check at n=0, 1, 2, exactly the range claimed in S10; N2 is a grid check of a degree-one polynomial identity, which decides such identities completely.

Verification and source binding

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

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

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