# 含初值邊界項的Fibonacci型OGF [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-analytic-ordinary-generating-function/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-analytic-ordinary-generating-function-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 在證明收斂的域內從遞迴推出OGF。 ordinary analytic OGF；不把formal identity任意代值。 ## 已知條件與符號 - work - G1 — a0=0、a1=1，所有n≥2有a_n=a_(n-1)+a_(n-2)；A(x)=sum_(n=0)^infinity a_n x^n。只在|x|<1/2推analytic等式。 - A(x) — a_n的ordinary生成函數 - [x^n]A — 係數a_n ## 規則與來源 - mko_definition · cited — coefficient extraction [x^n]A=a_n是編碼責任。有限partial sum只使用明示prefix。對a_n=r^n，A(x)=1/(1-rx)僅在|rx|<1成立。對a_n=a_{n-1}+a_{n-2}且初值a_0,a_1明示，A(x)=(a_0+(a_1-a_0)x)/(1-x-x^2)，boundary terms不可遺漏。formal power-series identity不自動是analytic equality；不得在radius外代值，有限coefficient prefix不決定完整OGF或radius，名稱中的analytic也不授權未證的逐項微分。 · mko-analytic-ordinary-generating-function - work · prerequisite — 數學歸納、幾何級數收斂與比較、absolute convergent series的index shift及有限線性組合；不假設OGF答案或逐項微分。 ## 逐步主鏈 S01 · implies操作前 a_0=0\le2^0,\quad a_1=1\le2^1 操作後 a_{n-1}\le2^{n-1},\ a_{n-2}\le2^{n-2}\implies a_n\le3\cdot2^{n-2}\le2^n 條件：無 規則：work · 依賴：G1, work 葉節點依據：work 以初值為base、遞迴為step，歸納證0≤a_n≤2^n。 S02 · implies操作前 |x|<1/2 操作後 \sum_{n=0}^{\infty}|a_nx^n|\le\sum_{n=0}^{\infty}(2|x|)^n<\infty 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work 幾何級數比較證absolute convergence，允許後面shift與有限相加。 S03 · implies操作前 A(x)=a_0+a_1x+\sum_{n=2}^{\infty}a_nx^n 操作後 A(x)=x+\sum_{n=2}^{\infty}a_{n-1}x^n+\sum_{n=2}^{\infty}a_{n-2}x^n 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 完整保留a0與a1x邊界後才代遞迴。 S04 · implies操作前 \sum_{n=2}^{\infty}a_{n-1}x^n 操作後 x\sum_{j=1}^{\infty}a_jx^j=x(A-a_0)=xA 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work j=n-1使下限為1，缺的a0明列後代0。 S05 · implies操作前 \sum_{n=2}^{\infty}a_{n-2}x^n 操作後 x^2\sum_{j=0}^{\infty}a_jx^j=x^2A 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work 第二shift下限0，正好是完整A。 S06 · implies操作前 A=x+xA+x^2A 操作後 (1-x-x^2)A=x 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 移項並把A因子提出。 S07 · implies操作前 |x+x^2|\le|x|+|x|^2<3/4<1 操作後 1-x-x^2\ne0,\quad A(x)=\frac{x}{1-x-x^2} 條件：無 規則：work · 依賴：G1, S06, work 葉節點依據：work 先證分母非零，再合法相除。 S08 · implies操作前 x=1/4 操作後 A(1/4)=\frac{1/4}{1-1/4-1/16}=4/11 條件：無 規則：work · 依賴：G1, S07, work 葉節點依據：work 1/4位於|x|<1/2，exact代值合法。 S09 · implies操作前 b_n=2^n,\quad B(x)=\sum_{n=0}^{\infty}(2x)^n 操作後 B(x)=1/(1-2x)\quad(|2x|<1) 條件：無 規則：work · 依賴：G1, S08, work 葉節點依據：work 另一geometric family明列analytic domain；x=1時原級數發散。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S09 · premise_audit · G1, S08, work — rational式在x=1給-1不等於發散級數的和。 - S08 · premise_audit · G1, S07, work — 沒有以有限partial sum冒充完整A值。 - S07 · premise_audit · G1, S06, work — 非零分母本身不代表原級數在域外收斂。 - S06 · premise_audit · G1, S05, work — 方程在已證收斂域內成立。 - S05 · premise_audit · G1, S04, work — 兩個shift的下限不同。 - S04 · premise_audit · G1, S03, work — shift先處理boundary再簡化。 - S03 · premise_audit · G1, S02, work — 不能直接把A寫成xA+x²A而漏x。 - S02 · premise_audit · G1, S01, work — 2|x|<1是明示domain責任。 - S01 · premise_audit · G1, work — 界涵蓋全部n，不從有限prefix猜radius。 ## 錯誤控制與反例 boundary terms兩次shift分別從j=1與j=0，保留a0差異。 analytic域先以 2^n 的幾何比較證明級數在 |x|<1/2 域內絕對收斂，再代入該域內的 1/4。 - A=xA+x²A即可，無需初值。 → reject — 漏a1x=x，會錯得A=0。 - B(1)=-1是2^n級數和。 → reject — |2x|=2≥1，原級數項不趨零。 - 前五個係數決定全部OGF。 → reject — 可在第六項改係數而不改前五項，故須全序列遞迴。 ## 結論與限制 |x|<1/2時A=x/(1-x-x²)，A(1/4)=4/11；未宣稱這是最大收斂域。 ## 驗證及來源綁定 2 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 11946fce17a53e461952d495d6db296e5a90c22948d207e1e3dc4fbe8a0af360 - original source SHA-256: e827f0cbbd48535760b49aca698318dc2d880c96facc8299c02ff8679c4d6b8d - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-analytic-ordinary-generating-function-01.json)