# A Fibonacci-type OGF with initial boundary terms

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-analytic-ordinary-generating-function/)

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-analytic-ordinary-generating-function-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Derive the OGF from a recurrence on a justified convergence domain.

An ordinary analytic OGF, not unrestricted evaluation of a formal identity.





## Givens and symbols


- work


- G1 — a0=0,a1=1 and a_n=a_(n-1)+a_(n-2) for all n≥2; A(x)=sum_(n=0)^infinity a_n x^n. Derive analytic identities only on|x|<1/2.


- A(x) — ordinary generating function of a_n
- [x^n]A — coefficient a_n





## Rules and sources


- mko_definition · cited — Coefficient extraction [x^n]A=a_n is the encoding obligation. A finite partial sum uses only its declared prefix. For a_n=r^n, A(x)=1/(1−r*x) holds analytically only when |r*x|<1. For a_n=a_(n−1)+a_(n−2) with explicit a0,a1, the OGF is (a0+(a1−a0)*x)/(1−x−x^2); initial boundary terms must not be omitted. A formal power-series identity is not automatically an analytic equality. Do not evaluate outside convergence, determine a whole OGF/radius from an unknown finite prefix or infer unproved termwise differentiation from the word analytic. · mko-analytic-ordinary-generating-function
- work · prerequisite — Induction, geometric convergence and comparison, index shifts and finite linear combinations of absolutely convergent series; neither the OGF answer nor termwise differentiation is assumed.





## Main derivation

S01 · impliesBefore

a_0=0\le2^0,\quad a_1=1\le2^1

After

a_{n-1}\le2^{n-1},\ a_{n-2}\le2^{n-2}\implies a_n\le3\cdot2^{n-2}\le2^n

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

The initial values form the base and recurrence the step proving0≤a_n≤2^n by induction.



S02 · impliesBefore

|x|<1/2

After

\sum_{n=0}^{\infty}|a_nx^n|\le\sum_{n=0}^{\infty}(2|x|)^n<\infty

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

Geometric comparison proves absolute convergence, permitting later shifts and finite sums.



S03 · impliesBefore

A(x)=a_0+a_1x+\sum_{n=2}^{\infty}a_nx^n

After

A(x)=x+\sum_{n=2}^{\infty}a_{n-1}x^n+\sum_{n=2}^{\infty}a_{n-2}x^n

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Retain a0 and a1x boundary terms before substituting the recurrence.



S04 · impliesBefore

\sum_{n=2}^{\infty}a_{n-1}x^n

After

x\sum_{j=1}^{\infty}a_jx^j=x(A-a_0)=xA

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

With j=n-1 the lower limit is 1; explicitly restore the missing a0 before substituting0.



S05 · impliesBefore

\sum_{n=2}^{\infty}a_{n-2}x^n

After

x^2\sum_{j=0}^{\infty}a_jx^j=x^2A

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

The second shift starts at 0 and gives the entire A.



S06 · impliesBefore

A=x+xA+x^2A

After

(1-x-x^2)A=x

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

Move terms and factor A.



S07 · impliesBefore

|x+x^2|\le|x|+|x|^2<3/4<1

After

1-x-x^2\ne0,\quad A(x)=\frac{x}{1-x-x^2}

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

Prove the denominator nonzero before division.



S08 · impliesBefore

x=1/4

After

A(1/4)=\frac{1/4}{1-1/4-1/16}=4/11

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

The point 1/4 lies in|x|<1/2, so exact evaluation is justified.



S09 · impliesBefore

b_n=2^n,\quad B(x)=\sum_{n=0}^{\infty}(2x)^n

After

B(x)=1/(1-2x)\quad(|2x|<1)

Conditions: none

Rule: work · Uses: G1, S08, work

Leaf basis: work

For the geometric family state the analytic domain explicitly; at x=1 the original series diverges.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S09 · premise_audit · G1, S08, work — The rational value -1 at x=1 is not a sum of the divergent series.
- S08 · premise_audit · G1, S07, work — No finite partial sum is substituted for the full A value.
- S07 · premise_audit · G1, S06, work — A nonzero denominator alone does not give convergence outside the domain.
- S06 · premise_audit · G1, S05, work — The equation holds on the justified convergence domain.
- S05 · premise_audit · G1, S04, work — The two shifts have different lower limits.
- S04 · premise_audit · G1, S03, work — Handle the boundary before simplifying the shift.
- S03 · premise_audit · G1, S02, work — Do not write A=xA+x²A and omit x.
- S02 · premise_audit · G1, S01, work — The domain obligation2|x|<1 is explicit.
- S01 · premise_audit · G1, work — The bound covers all n rather than guessing a radius from a prefix.





## Error controls and negative controls

Boundary termsThe shifts start at j=1 and j=0; retain the a0 difference.

Analytic domainFirst use the 2^n geometric comparison to prove absolute convergence on |x|<1/2, then evaluate at the point 1/4 inside that domain.


- A=xA+x²A needs no initial values. → reject — It omits a1x=x and incorrectly yields A=0.
- B(1)=-1 sums the2^n series. → reject — Here|2x|=2≥1 and the series terms do not tend to zero.
- The first five coefficients determine the whole OGF. → reject — Changing a later coefficient preserves the first five, so an all-index recurrence is needed.





## Result and limitations

For|x|<1/2, A=x/(1-x-x²) and A(1/4)=4/11; no maximal-domain claim is made.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 11946fce17a53e461952d495d6db296e5a90c22948d207e1e3dc4fbe8a0af360
- original source SHA-256: e827f0cbbd48535760b49aca698318dc2d880c96facc8299c02ff8679c4d6b8d
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-analytic-ordinary-generating-function-01.json)