仿射索引的全稱子數列證書

目標與範圍

由 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 在整個非負整數域嚴格遞增；指標合成先算內層。

逐步主鏈

j\in\mathbb N_0

k(j)=1+2j\in\mathbb N_0

j_2>j_1\ge0

k(j_2)-k(j_1)=2(j_2-j_1)>0

b_j=a_{k(j)}

b_j=3(1+2j)-2=1+6j

b_j=a_{k(j)},\quad k\text{ strictly increasing on }\mathbb N_0

(b_j)\text{ is an infinite subsequence of }(a_n)

i_2>i_1\ge0

\ell(i_2)-\ell(i_1)=3(i_2-i_1)>0

m(i)=k(\ell(i))

m(i)=1+2(2+3i)=5+6i

c_i=b_{\ell(i)}=a_{m(i)}

c_i=13+18i

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}

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, S04 — r(1)<r(0) 是明確失敗，而非有限樣本無法判定。
• S07 · premise_audit · S03, S06 — 等式核值，正步長另核次序。
• S06 · inverse_equivalence · G1, S05 — 定義的組合次序是先 ell 後 k；這兩條特定仿射律數值恰好可交換，但一般索引映射不能如此互換。
• S05 · premise_audit · G1 — 起點 2 非負，步長 3 正。
• S04 · premise_audit · S01, S02, S03 — 有限前綴本身不提供這個全函數。
• S03 · inverse_equivalence · G1, S02 — 代回 a 的下標確為 k(j)。
• S02 · premise_audit · G1, S01 — 單射雖由此推出，反向卻不足。
• S01 · premise_audit · G1 — 不是只列前幾個索引。

錯誤控制與反例

索引先行

先代 k(j) 再算 a，保留括號。

無限證書

用正步長差值證全部索引，而非有限表。

• 單射索引就必為子數列。 → reject — S08 的交換單射不遞增。
• c_i 的來源索引是 k(i)。 → reject — 正確索引 k(ell(i))=5+6i；k(i)=1+2i，在 i=0 已是 5 與 1。
• 前十索引遞增已證無限子數列。 → reject — 仍需整個 N_0 上的映射及遞增證書。

結論與限制

b_j=1+6j、c_i=13+18i；兩者均由完整嚴格遞增索引證書構成。

驗證及來源綁定

1 個本稿宣告算術檢查；只支持所列算式。

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 723f86ede56e20fd17954f55eaf9ac1bb183cabb027071619eab37816d8ea520
• original source SHA-256: b3f9513bca7f0ae4d56cfc0a6777cfda19771c065785d1014d30696c2f912b93
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

同源完整 JSON（含公式、AST、反控制與修訂記錄）