凸盒中的全稱路徑與拼接

目標與範圍

證 [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] 上連續、端點正確且全範圍在空間內的映射；每對點皆有路徑才路徑連通。

逐步主鏈

0\le t\le1

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

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\})

\gamma(0),\gamma(1)

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

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

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

x,y\in B\text{ arbitrary}

B\text{ is path connected}

\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)

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

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

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

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

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）