振盪尾的兩個收斂子數列

目標與範圍

對 a_n=(-1)^n+1/(n+1) 給有界性與兩個完整收斂子數列。

只證宣告的符號數列實例，不以其替代一般 BW 定理。

已知條件與符號

• algebra
• epsilon

• G1 — a_n=(-1)^n+1/(n+1)，n≥0；索引取 k(j)=2j、ell(j)=2j+1。

• k,\ell — 偶奇索引
• M — 全序列界

規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。

• mko_definition · cited — bounded 須為 exists M forall n；subsequence index genuinely strictly increasing 且無限，並有 forall-tail epsilon witness。週期列與 oscillatory rational tails 提供 exact slices。有限 prefix／cluster search 不足；定理不保證原數列收斂，也不保證不同收斂子數列的極限相同。 · mko-bolzano-weierstrass-theorem-real
• algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
• epsilon · prerequisite — 收斂表示每個正 epsilon 有一個整數 N，使全部 n≥N 的誤差嚴格小於 epsilon；使用實數 Archimedean 性。

逐步主鏈

|(-1)^n|=1,\quad0<1/(n+1)\le1

|a_n|\le2\quad\forall n\ge0

k(j+1)-k(j)=2,\quad\ell(j+1)-\ell(j)=2

k,\ell:\mathbb N_0\to\mathbb N_0\text{ strictly increasing}

a_{k(j)}=a_{2j}

a_{2j}=1+1/(2j+1)

\varepsilon>0,\quad J=\lfloor1/\varepsilon\rfloor+1

j\ge J\Longrightarrow |a_{2j}-1|=1/(2j+1)<\varepsilon

a_{\ell(j)}=a_{2j+1}

a_{2j+1}=-1+1/(2j+2)

j\ge J=\lfloor1/\varepsilon\rfloor+1

|a_{2j+1}+1|=1/(2j+2)<\varepsilon

a_{2j}\to1,\quad a_{2j+1}\to-1

(a_n)\text{ has convergent subsequences with different limits}

1\ne-1

(a_n)\text{ does not converge}

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · S04, S06 — 只由不同已證子極限否定原收斂，不因振盪外觀猜測。
• S07 · premise_audit · S01, S02, S04, S06 — 實例論證沒有聲稱所有有界數列都已由有限測試證明。
• S06 · premise_audit · S05 — 這是獨立核奇序列，非從偶序列推相同極限。
• S05 · inverse_equivalence · G1, S02 — 極限為 -1 而不是絕對值 1。
• S04 · premise_audit · S03 — 嚴格界對所有 j≥J。
• S03 · inverse_equivalence · G1, S02 — 分母是 2j+1，不是 2j。
• S02 · premise_audit · G1 — 無限定義域已明示，不是有限索引列表。
• S01 · premise_audit · G1 — 不是以 prefix 最大值代替全稱有界性。

錯誤控制與反例

全序列有界

M 必對每個 n 成立。

子列三責任

索引嚴格遞增、無限、且有全尾收斂界。

• BW 保證原數列收斂。 → reject — 本例兩個已證子極限不同。
• 所有收斂子數列極限必相同。 → reject — 此例的 1 與 -1 不同。
• 看到有限重複值就證 BW。 → reject — 仍需完整無限索引、全序列界及全尾證書。

結論與限制

全序列有界，偶子列趨 1、奇子列趨 -1，所以原列不收斂。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: f1198b016a1e24a4b4724094afffa9b2aa9f46a46781515f4f078244bea62398
• original source SHA-256: 605ab67bfeb763ae5cddd56fa58c8fa84b2fbce158ebd93195090c891bdf3c42
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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