有限度量的完整收縮證書

目標與範圍

在三點離散度量與常值 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 性。

逐步主鏈

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)

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

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

(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

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

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

x,y\in X

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

Tx=x

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

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

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

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

局部子步與引理

本稿無局部子步。

逐步反向審查

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