# 有限度量的完整收縮證書

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

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

derivation-mko-contraction-mapping-theorem-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

在三點離散度量與常值 self-map 上核完備、唯一不動點及誤差界。

只證完整有限模型，不從此取代一般 Banach 定理。





## 已知條件與符號


- algebra
- sets
- epsilon


- G1 — X={a,b,c}，d(x,x)=0、異點 d=1；T(a)=T(b)=T(c)=a，q=1/2，x_0=c。


- D — 完整度量矩陣
- T — 全 self-map
- q — 嚴格收縮常數





## 規則與來源


- mko_definition · cited — 題族以完整finite metric與total self-map逐對驗d(Tx,Ty)≤q d(x,y)，固定0≤q<1。從任意x0完整產生Picard orbit，枚舉fixed points並核唯一性；exact rational metric下驗d(x_n,x*)≤q^n/(1-q)d(x_1,x_0)。finite metric自動complete但只證指定模型；q=1、非self-map、非complete空間與sampled-pairs不足均不得套定理。 · mko-contraction-mapping-theorem
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- epsilon · prerequisite — 收斂表示每個正 epsilon 有一個整數 N，使全部 n≥N 的誤差嚴格小於 epsilon；使用實數 Archimedean 性。





## 逐步主鏈

S01 · implies操作前

D=\begin{pmatrix}0&1&1\\1&0&1\\1&1&0\end{pmatrix}

操作後

d\ge0,\quad d(x,y)=0\iff x=y,\quad d(x,y)=d(y,x)

條件：無

規則：sets · 依賴：G1

葉節點依據：sets

完整九項矩陣直接核非負、分離及對稱。



S02 · implies操作前

x=z\text{ or }x\ne z

操作後

d(x,z)\le d(x,y)+d(y,z)

條件：無

規則：algebra · 依賴：G1, S01

葉節點依據：algebra

x=z 時左邊零；異點時右邊不可能兩項同為零，所以至少 1。這涵蓋全部 27 三元組。



S03 · implies操作前

(z_n)\text{ is }d\text{-Cauchy},\quad\varepsilon=1/2

操作後

\exists N\ \forall m,n\ge N:\ d(z_m,z_n)<1/2\Longrightarrow z_m=z_n

條件：無

規則：epsilon · 依賴：S01, S02

葉節點依據：epsilon

Cauchy 尾項只能全相同，故最終常值於 X 內並收斂，空間完備。



S04 · implies操作前

T(a)=T(b)=T(c)=a\in X

操作後

T:X\to X\text{ is a total self-map}

條件：無

規則：sets · 依賴：G1

葉節點依據：sets

逐一核全部三個輸入且像仍在載體。



S05 · implies操作前

x,y\in X

操作後

d(Tx,Ty)=0\le\tfrac12d(x,y),\quad0\le q<1

條件：無

規則：algebra · 依賴：G1, S04

葉節點依據：algebra

所有九個有序點對像相等，所以完整收縮不等式成立。



S06 · implies操作前

Tx=x

操作後

x=a\text{ is the only fixed point}

條件：無

規則：sets · 依賴：G1, S04

葉節點依據：sets

a 映到自己；b,c 映到不同點 a，完整不動點枚舉只剩 a。



S07 · implies操作前

x_{n+1}=Tx_n,\quad x_0=c

操作後

x_1=a,\quad x_n=a\ (n\ge1),\quad x_n\to a

條件：無

規則：sets · 依賴：G1, S04, S06

葉節點依據：sets

第一步到 a，之後用 T(a)=a 歸納整個無限 orbit。



S08 · implies操作前

\frac{q^n}{1-q}d(x_1,x_0)=2^{1-n}

操作後

d(x_0,a)=1\le2;\quad d(x_n,a)=0\le2^{1-n}\ (n\ge1)

條件：無

規則：algebra · 依賴：S06, S07

葉節點依據：algebra

逐分支核全 n 的標準幾何誤差界，包括 n=0。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S06, S07 — 界支持本例，並不以此有限度量論證一般完備空間定理。
- S07 · premise_audit · G1, S04, S06 — 不是只產生有限 Picard trace 就宣稱收斂。
- S06 · premise_audit · G1, S04 — 唯一性由全部點核對，亦可由 d≤q d 及 q<1 推出。
- S05 · premise_audit · G1, S04 — q=1/2 嚴格小於 1；不是僅非擴張 q=1。
- S04 · premise_audit · G1 — 定理所需 self-map 不是任意去別空間的映射。
- S03 · premise_audit · S01, S02 — 所有 Cauchy 序列由最小正距離控制，不是幾條樣本。
- S02 · premise_audit · G1, S01 — 三角不等式有全三元組論證，非數值抽樣。
- S01 · premise_audit · G1 — 不是只給若干點對距離。





## 錯誤控制與反例

度量全表先核全部公理及全域映射，再核收縮。

全 orbit由固定點後歸納永遠固定，與有限 trace 分開。


- q=1 的恆等映射也必唯一不動點。 → reject — 三個點皆固定，嚴格收縮前提失敗。
- 只核 (a,b) 就證所有點對收縮。 → reject — 全點對量詞不能由一對成功取代。
- 映射離開 X 仍可使用 self-map 定理。 → reject — 迭代及不動點責任須在同一 X。





## 結論與限制

此有限度量完備，T 的唯一不動點 a；從 c 一步到達，全部誤差界成立。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 9495e80b14cbe0e32e555d76b8ebed0ff8eb48f593477974ab06adb8325a82a6
- original source SHA-256: 9495e80b14cbe0e32e555d76b8ebed0ff8eb48f593477974ab06adb8325a82a6
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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