# 仿射索引的全稱子數列證書 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-subsequence/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-subsequence-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 由 a_n=3n-2、k(j)=1+2j 構造並再取子數列。 n,j≥0 整數；完整仿射索引，不以有限前綴或任意重排代替。 ## 已知條件與符號 - algebra - sets - definition_here - G1 — a_n=3n-2（n≥0）；k(j)=1+2j；另一索引 ell(i)=2+3i（i≥0）。 - k,\ell,m — 索引映射 - b_j,c_i — 選出的項 ## 規則與來源 - mko_definition · cited — 索引k:N→N必須strictly increasing，不只是injective；b_j=a_{k(j)}。本輪以affine k(j)=s+dj、d>=1給通用symbolic certificate，並區分有限遞增prefix與真正無限subsequence。重排、任意子集合或finite sample都不是自動的subsequence證書。 · mko-subsequence - algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。 - sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。 - definition_here · prerequisite — b_j=a_{k(j)} 是子數列須 k 在整個非負整數域嚴格遞增；指標合成先算內層。 ## 逐步主鏈 S01 · implies操作前 j\in\mathbb N_0 操作後 k(j)=1+2j\in\mathbb N_0 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra k 把全部非負整數送到合法來源索引。 S02 · implies操作前 j_2>j_1\ge0 操作後 k(j_2)-k(j_1)=2(j_2-j_1)>0 條件：無 規則：algebra · 依賴：G1, S01 葉節點依據：algebra 對任意兩個有序索引證嚴格遞增。 S03 · equivalent操作前 b_j=a_{k(j)} 操作後 b_j=3(1+2j)-2=1+6j 條件：無 規則：algebra · 依賴：G1, S02 葉節點依據：algebra 先算 k(j)，再代入來源數列，不能把 k 當值。 S04 · definition操作前 b_j=a_{k(j)},\quad k\text{ strictly increasing on }\mathbb N_0 操作後 (b_j)\text{ is an infinite subsequence of }(a_n) 條件：無 規則：definition_here · 依賴：S01, S02, S03 葉節點依據：definition_here 完整無限索引映射和取項公式共同構成子數列定義。 S05 · implies操作前 i_2>i_1\ge0 操作後 \ell(i_2)-\ell(i_1)=3(i_2-i_1)>0 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra 第二索引亦合法非負且嚴格遞增。 S06 · equivalent操作前 m(i)=k(\ell(i)) 操作後 m(i)=1+2(2+3i)=5+6i 條件：無 規則：algebra · 依賴：G1, S05 葉節點依據：algebra 組合索引仍是非負仿射函數。 S07 · implies操作前 c_i=b_{\ell(i)}=a_{m(i)} 操作後 c_i=13+18i 條件：無 規則：algebra · 依賴：S03, S06 葉節點依據：algebra 兩種取項路徑都給 13+18i，且 m 的正步長 6 證仍為來源子數列。 S08 · implies操作前 r(0)=1,\ r(1)=0,\ r(j)=j\ (j\ge2) 操作後 r\text{ injective but not increasing};\quad(a_{r(j)})\text{ is not certified as a subsequence} 條件：無 規則：sets · 依賴：G1, S04 葉節點依據：sets 交換前兩索引給無限單射反例，顯示單射不等於保次序。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S04 — r(1)