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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-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-sequence-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

(a_n)

After

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

Conditions: 0\in\mathbb{N}

Rule: mko_seq_def · Uses: G1, G2, mko_seq_def

Leaf basis: mko_seq_def + function_def

By the MKO a sequence is a function with domain ℕ: the index n is the input and a_n the output. The given information is a recurrence with an initial condition; it constrains the values of a but does not yet say that such an a exists or is unique, which is what S02 to S06 prove.



S02 · definitionBefore

n\in\mathbb{N}

After

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

Conditions: none

Rule: def_intro · Uses: S01

Leaf basis: def_intro + function_def

Propose the candidate sequence s_n=5+3n. For each natural number n, 5+3n is a single well-defined real number, so s is a function ℕ→ℝ, that is, a sequence.



S03 · equivalentBefore

s_0

After

s_0=5+3\cdot 0=5

Conditions: none

Rule: eq_replace · Uses: S02

Leaf basis: eq_replace + mul_zero + add_zero

Substitute n=0: 3·0=0 (multiplication by zero) and 5+0=5 (additive identity), so s₀=5, as the initial condition requires.



S04 · equivalentBefore

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

After

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

Conditions: none

Rule: distributive · Uses: S02

Leaf basis: distributive + add_assoc + mul_one

For any n: 5+3(n+1)=5+(3n+3) by distributivity, =(5+3n)+3 by associativity, =s_n+3. So s satisfies the recurrence, as an identity valid for every n.



S05 · impliesBefore

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

After

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

Conditions: none

Rule: exists_intro · Uses: S02, S03, S04

Leaf basis: exists_intro + and_intro_elim

s is a sequence (S02) satisfying the initial condition (S03) and the recurrence (S04), so at least one sequence satisfies G2. Existence is obtained by exhibiting an example.



S06 · theorem_applicationBefore

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

After

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

Conditions: none

Rule: L_unique · Uses: S01, S02, L_unique, function_def

Leaf basis: L_unique + function_def + nat_induction

By Lemma L_unique, proved by induction in S06.1 and S06.2, every sequence satisfying G2 agrees with s at every index; both have domain ℕ and codomain ℝ, so a=s by function_def. Together with S05, exactly one such sequence exists.



S07 · impliesBefore

a_n=5+3n

After

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

Conditions: none

Rule: forall_elim · Uses: S06

Leaf basis: forall_elim + numeric_evaluation

Substitute n=0, 1, 2, 3, 4 and 10 into the general term: 5, 8, 11, 14, 17 and 35. The initial term is a₀=5 (index 0), not a₁.



S08 · impliesBefore

a_{10}=35

After

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

Conditions: none

Rule: def_unfold · Uses: S07, G1

Leaf basis: def_unfold + numeric_evaluation

The indices 0 to 10 number 11, so a₁₀ is the 11th value when counting from 1. If someone uses the 1-based labels b_k=a_{k−1} (k≥1, so b₁=a₀=5), their 'tenth term' is b₁₀=a₉=5+27=32, not a₁₀=35. Speaking of 'the tenth term' requires saying whether indexing starts at 0 or at 1.



S09 · definitionBefore

L=4

After

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

Conditions: 0\leq n<4

Rule: mko_seq_def · Uses: G3, S07, mko_seq_def

Leaf basis: mko_seq_def + set_builder

The finite sequence of length L=4 has index set {n∈ℕ ∣ n<4}={0,1,2,3}; it is a function {0,1,2,3}→ℝ with values 5, 8, 11, 14. The index 4 is not permitted (4<4 fails), so this finite sequence has no a₄, even though the infinite sequence has a₄=17.



S10 · impliesBefore

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

After

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

Conditions: none

Rule: mul_zero · Uses: S07

Leaf basis: mul_zero + add_zero + numeric_evaluation

Consider another sequence c_n=5+3n+n(n−1)(n−2). For n=0, 1, 2 one factor of the product n(n−1)(n−2) is 0, so the product is 0 and c_n=5+3n. Hence c has exactly the same prefix 5, 8, 11 as a.



S11 · impliesBefore

c_3

After

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

Conditions: none

Rule: function_def · Uses: S07, S10, function_def

Leaf basis: function_def + numeric_evaluation

c₃=5+3·3+3·2·1=14+6=20, while a₃=14. The two sequences differ at index 3, so c≠a by function_def. Hence the prefix 5, 8, 11 does not determine the sequence: at least two different sequences begin with it.



S12 · impliesBefore

c_3-c_2

After

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

Conditions: none

Rule: contrapositive · Uses: S06, S10, S11

Leaf basis: contrapositive + numeric_evaluation

c satisfies c₀=5 but fails the recurrence at n=2: c₃−c₂=9≠3. This agrees with S06: only a satisfies both the initial condition and the recurrence. What determines the sequence is the rule together with the initial condition, not finitely many first terms.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S05, S06, S07, S08, S09, S11

Leaf basis: and_intro_elim

Goal (1) is completed by S05 and S06, (2) by S07 and S08, (3) by S09, and (4) by S10 and S11.







## Substeps and lemmas

S06.1 · induction_baseBefore

a_0=5

After

a_0=s_0

Conditions: none

Rule: eq_refl_symm_trans · Uses: S02, S03

Leaf basis: eq_refl_symm_trans

Base case: a₀=5 by the initial condition and s₀=5 by S03, so a₀=s₀.



S06.2 · induction_stepBefore

a_n=s_n

After

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

Conditions: n\in\mathbb{N}\ \text{arbitrary}

Rule: eq_replace · Uses: S04, nat_induction

Leaf basis: eq_replace + nat_induction + forall_elim

Suppose a_n=s_n for some n. Then a_{n+1}=a_n+3 by the recurrence for a, =s_n+3 by replacing with the induction hypothesis, =s_{n+1} by S04. By induction from n₀=0, S06.1 and S06.2 prove Lemma L_unique.







## 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 1The 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 sequenceThe 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−1The 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-sequence-01.json)