# 振盪尾的兩個收斂子數列 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-bolzano-weierstrass-theorem-real/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-bolzano-weierstrass-theorem-real-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 對 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 性。 ## 逐步主鏈 S01 · implies操作前 |(-1)^n|=1,\quad0<1/(n+1)\le1 操作後 |a_n|\le2\quad\forall n\ge0 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra 三角界給同一 M=2 控制全部項。 S02 · implies操作前 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} 條件：無 規則：algebra · 依賴：G1 葉節點依據：algebra 兩個仿射完整索引均步長正且起點非負。 S03 · equivalent操作前 a_{k(j)}=a_{2j} 操作後 a_{2j}=1+1/(2j+1) 條件：無 規則：algebra · 依賴：G1, S02 葉節點依據：algebra 偶指數符號為正，先代索引再算值。 S04 · implies操作前 \varepsilon>0,\quad J=\lfloor1/\varepsilon\rfloor+1 操作後 j\ge J\Longrightarrow |a_{2j}-1|=1/(2j+1)<\varepsilon 條件：無 規則：epsilon · 依賴：S03 葉節點依據：epsilon 共同分母下界給全部偶子數列尾端趨 1。 S05 · equivalent操作前 a_{\ell(j)}=a_{2j+1} 操作後 a_{2j+1}=-1+1/(2j+2) 條件：無 規則：algebra · 依賴：G1, S02 葉節點依據：algebra 奇指數符號為負，仍保留正的有理擾動。 S06 · implies操作前 j\ge J=\lfloor1/\varepsilon\rfloor+1 操作後 |a_{2j+1}+1|=1/(2j+2)<\varepsilon 條件：無 規則：epsilon · 依賴：S05 葉節點依據：epsilon 同一 J 亦足夠控制奇子數列的所有尾項。 S07 · implies操作前 a_{2j}\to1,\quad a_{2j+1}\to-1 操作後 (a_n)\text{ has convergent subsequences with different limits} 條件：無 規則：epsilon · 依賴：S01, S02, S04, S06 葉節點依據：epsilon 符合 BW 存在某個子數列的結論，此具體模型還給出兩個。 S08 · implies操作前 1\ne-1 操作後 (a_n)\text{ does not converge} 條件：無 規則：epsilon · 依賴：S04, S06 葉節點依據：epsilon 若原數列收斂至 L，任意嚴格遞增索引最終超過原 N，兩子數列都應趨 L；極限唯一性矛盾。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-bolzano-weierstrass-theorem-real-01.json)