# 凸盒中的全稱路徑與拼接

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-path-connected-space/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-path-connected-space-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

證 [0,1]^2 路徑連通，並核兩段路徑的接點。

通常實拓撲與明示線性路徑；不把連通一般反推路徑連通。





## 已知條件與符號


- sets
- algebra
- polynomial
- pasting
- definition_here


- G1 — B=[0,1]^2；任意 x=(x_1,x_2),y=(y_1,y_2)∈B，路徑定義域為通常拓撲的 [0,1]。


- \gamma — 仿射路徑
- \eta — 拼接路徑





## 規則與來源


- mko_definition · cited — path是continuous gamma:[0,1]→X且gamma(0)=x、gamma(1)=y。exact families以實interval與finite-dimensional box的linear path、兩條path的piecewise concatenation核endpoint、range與接點；disconnected gap與兩點discrete space用connected-image責任排除。只給有限sample points、只對某一對端點有path或忽略continuity都不證path connected。path connected推出connected，但一般converse不成立。 · mko-path-connected-space
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- polynomial · prerequisite — 多項式在實數上連續且可逐項微分；d(x^k)/dx=k x^(k-1)，常數導數為零。
- pasting · prerequisite — 有限閉覆蓋上連續且在交集相合的映射可拼接為連續映射；[0,1] 在通常拓撲連通。
- definition_here · prerequisite — 路徑是 [0,1] 上連續、端點正確且全範圍在空間內的映射；每對點皆有路徑才路徑連通。





## 逐步主鏈

S01 · definition操作前

0\le t\le1

操作後

\gamma(t)=(1-t)x+ty

條件：無

規則：definition_here · 依賴：G1

葉節點依據：definition_here

對任意端點明示一條完整函數，而非有限點列。



S02 · implies操作前

0\le x_i,y_i,t\le1

操作後

0\le(1-t)x_i+ty_i\le(1-t)+t=1\quad(i\in\{1,2\})

條件：t\in[0,1]

規則：algebra · 依賴：G1, S01

葉節點依據：algebra

非負權重和為一，兩個座標都留在盒中。



S03 · equivalent操作前

\gamma(0),\gamma(1)

操作後

\gamma(0)=x,\quad\gamma(1)=y

條件：無

規則：algebra · 依賴：S01

葉節點依據：algebra

代入端點得指定起終點。



S04 · implies操作前

\gamma_i(t)=(1-t)x_i+ty_i

操作後

\gamma:[0,1]\to B\text{ continuous}

條件：無

規則：polynomial · 依賴：S01, S02

葉節點依據：polynomial

每座標為仿射多項式，連續；Euclidean 距離下可由差值範數 |t-s|‖y-x‖直接核。



S05 · definition操作前

x,y\in B\text{ arbitrary}

操作後

B\text{ is path connected}

條件：無

規則：definition_here · 依賴：G1, S02, S03, S04

葉節點依據：definition_here

每對點均有已核端點、連續性和全範圍的路徑，完成全稱定義。



S06 · implies操作前

\alpha(1)=\beta(0),\quad\eta(t)=\begin{cases}\alpha(2t)&t\le1/2\\\beta(2t-1)&t\ge1/2\end{cases}

操作後

\eta(1/2)=\alpha(1)=\beta(0)

條件：\alpha,\beta:[0,1]\to B\text{ continuous},\ \alpha(1)=\beta(0)

規則：pasting · 依賴：G1

葉節點依據：pasting

兩條在 B 內的連續路徑若接點相同，可用重參數化拼接。



S07 · theorem_application操作前

[0,1]=[0,1/2]\cup[1/2,1]

操作後

\eta\text{ continuous},\quad\eta(0)=\alpha(0),\ \eta(1)=\beta(1)

條件：無

規則：pasting · 依賴：S06

葉節點依據：pasting

兩閉段覆蓋定義域，接點相合，套有限閉拼接引理，範圍仍在 B。



S08 · implies操作前

B=U\cup V\text{ a hypothetical nonempty open separation}

操作後

\gamma^{-1}(U),\gamma^{-1}(V)\text{ would separate }[0,1]\text{, contradiction}

條件：無

規則：pasting · 依賴：S05

葉節點依據：pasting

取分離兩側各一點，路徑逆像給非空不交開覆蓋，與區間連通矛盾，所以 B 亦連通。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S05 — 只證路徑連通推出連通，未聲稱一般逆命題。
- S07 · premise_audit · S06 — 沒有忽略 t=1/2 的一致性。
- S06 · premise_audit · G1 — 此為另加條件的拼接，必須核共有接點。
- S05 · premise_audit · G1, S02, S03, S04 — 任意 x,y 的前提不能由一對成功取代。
- S04 · premise_audit · S01, S02 — 若 x=y 是常值映射，連續仍成立。
- S03 · inverse_equivalence · S01 — 端點正確不取代連續與全範圍責任。
- S02 · premise_audit · G1, S01 — 這是全部 t 的範圍證書，不是抽樣。
- S01 · premise_audit · G1 — 每個 t 都有同型兩座標值。





## 錯誤控制與反例

全參數範圍用凸組合不等式核全部 t。

三責任端點、連續性與範圍須分別成立。


- 端點符合指定起終點，就自動是連續路徑。 → reject — 跳躍函數可有正確端點但不連續。
- R\{0} 可由 -1 路徑走到 1。 → reject — IVT 迫使路徑取值 0，違反範圍。
- 任意兩條路徑不核接點即可拼接。 → reject — 左右極限若不同，拼接在中點不連續。





## 結論與限制

盒 B 路徑連通且連通；拼接需接點相合。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 701fe48ba785ed68079f5db1ab929c8a020f370f85231cf4297cb7d1ac25d02f
- original source SHA-256: 06bc539cd56d730fd9c0e4e20739eb4fa511ae175466c09a3cd9651ac78ba03a
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-path-connected-space-01.json)