# oldest-to-newest二階遞迴trace [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-recurrence-relation/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-recurrence-relation-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 對齊state、係數與全部初值，生成a5並證唯一性責任。 有限exact integer trace；不猜closed form。 ## 已知條件與符號 - work - G1 — order r=2，initial_values=(a0,a1)=(1,3)，coefficients=(2,1)，constant=1；所有n≥2用a_n=1+2a_(n-2)+a_(n-1)。 - A_n — 最近兩項state - F — shift-append update ## 規則與來源 - mko_definition · cited — r階遞迴須有全部r個初值，係數由最舊到最新對齊；狀態左移後附加新項。有限前綴不證閉式、收斂或漸近性。 · mko-recurrence-relation - work · prerequisite — order-r state按最舊到最新排列；single-valued整數update為total；數學歸納可從全部初值推唯一性。 ## 逐步主鏈 S01 · implies操作前 A_1=(a_0,a_1)=(1,3) 操作後 F(u,v)=(v,1+2u+v) 條件：無 規則：work · 依賴：G1, work 葉節點依據：work 最舊u乘2、最新v乘1，再左移append。 S02 · implies操作前 a_2=1+2(1)+3 操作後 a_2=6,\quad A_2=(3,6) 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work 第一次update保留舊最新3作新state第一項。 S03 · implies操作前 a_3=1+2(3)+6 操作後 a_3=13,\quad A_3=(6,13) 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 從A2正確對齊求下一項。 S04 · implies操作前 a_4=1+2(6)+13 操作後 a_4=26,\quad A_4=(13,26) 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work 再次shift後append26。 S05 · implies操作前 a_5=1+2(13)+26 操作後 a_5=53,\quad A_5=(26,53) 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work 有限target index5已完整生成。 S06 · implies操作前 a_0=b_0,\ a_1=b_1\quad\text{and same recurrence} 操作後 (a_{n-2},a_{n-1})=(b_{n-2},b_{n-1})\implies a_n=b_n 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 同一single-valued update把相同前兩項送到相同下一項。 S07 · implies操作前 a_0=b_0=1,\ a_1=b_1=3 操作後 a_n=b_n\quad\text{for every }n\ge0 條件：無 規則：work · 依賴：G1, S06, work 葉節點依據：work 以兩初值為基礎、上一項推導為step，數學歸納給唯一序列。 S08 · implies操作前 a_0=1\text{ only},\quad a_1=t 操作後 a_2=3+t\text{ depends on }t 條件：無 規則：work · 依賴：G1, S07, work 葉節點依據：work 缺第二初值時，不同t產生不同合法序列，不能稱唯一。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S07, work — 有限trace完成不宣稱收斂或漸近。 - S07 · premise_audit · G1, S06, work — 唯一性不等於已證closed form或growth rate。 - S06 · premise_audit · G1, S05, work — 歸納基礎需要兩個初值，不能只有一個。 - S05 · premise_audit · G1, S04, work — 每個中間值為明示安全整數。 - S04 · premise_audit · G1, S03, work — constant1在每次update都存在。 - S03 · premise_audit · G1, S02, work — 係數2乘3而非6。 - S02 · premise_audit · G1, S01, work — state不是只記新scalar6。 - S01 · premise_audit · G1, work — 不能倒轉係數為u+2v。 ## 錯誤控制與反例 係數對齊(2,1)分別乘a_(n-2)、a_(n-1)。 state width每次state保留兩項，先shift再append。 - a2=1+1+2乘3=8。 → reject — 係數順序最舊乘2，正確值6。 - 只給a0=1已唯一。 → reject — a1=t時a2=3+t仍自由。 - 六項上升已證發散。 → reject — 有限prefix不能證無限tail性質。 ## 結論與限制 prefix為1、3、6、13、26、53；兩初值加total rule確定唯一序列。 ## 驗證及來源綁定 2 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 124f407c6762352d6b2a2e969d2d845466e4482a03a8f31e13b95650c4a212a5 - original source SHA-256: 22806b93c67d3eddec49366fb95886552a6c5b9b138df147ef955ed07c293e53 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-recurrence-relation-01.json)