# 實 Banach 空間：(ℝ², ℓ¹) 的範數、誘導度量與完備性

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

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

derivation-mko-real-banach-space-01 · production-20261019-adopted-96



## 目標與範圍

在 V=ℝ² 上取 ℓ¹ 範數 ‖x‖₁=|x₁|+|x₂| 與同一範數誘導的度量 d₁(x,y)=‖x−y‖₁。（一）證明 ‖·‖₁ 是範數、d₁ 是度量，並算出 d₁((3,−1),(1,2))。（二）由實數的 Cauchy 完備性完整證明 (ℝ²,d₁) 完備，所以 (ℝ²,‖·‖₁) 是實 Banach 空間；並引用有限維實賦範空間完備的命名定理。（三）證明 ‖·‖₁ 不滿足平行四邊形律，所以不是由任何內積誘導。

在 MKO 的範圍內工作：明示的有限維 ℝ²、命名的 ℓ¹ 範數，度量必須由同一範數誘導（假設 a1）；完備性以證明加命名定理證書處理，不以有限條 Cauchy 序列抽樣代替（假設 a2）。本稿完整證明 n=2、ℓ¹ 的特例，只假設實數的 Cauchy 完備性；一般有限維情形（含 ℓ^∞）引用命名定理。不處理無限維 Banach 空間或 Hilbert 空間理論，不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- abs_rules
- order_basics
- vector_space_axioms
- completeness_axiom
- numeric_evaluation


- G1 — V=ℝ²，加法與實數倍數逐坐標進行，是實向量空間。
- G2 — ‖x‖₁=|x₁|+|x₂|；度量取同一範數誘導的 d₁(x,y)=‖x−y‖₁，不使用其他度量。
- G3 — 數值例：x=(3,−1)、y=(1,2)；平行四邊形律的例子 u=(1,0)、v=(0,1)。


- \|x\|_1=|x_1|+|x_2| — ℝ² 上的 ℓ¹ 範數
- d_1(x,y)=\|x-y\|_1 — 由同一範數誘導的度量
- \|x\|_\infty=\max(|x_1|,|x_2|) — ℓ^∞ 範數，只作對照
- (x^{(m)})_{m\ge 1} — ℝ² 中的序列，坐標 x^{(m)}_k
- a=(a_1,a_2) — 候選極限
- \varepsilon,\ N — 收斂與 Cauchy 定義中的容許誤差與門檻





## 規則與來源


- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。
- completeness_axiom · prerequisite — 實數完備性：ℝ 的每個非空且有上界的子集都有最小上界（上確界）。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- metric_def · prerequisite — 度量：d:X×X→ℝ 滿足 d(x,y)≥0 且 d(x,y)=0 ⇔ x=y；d(x,y)=d(y,x)；三角不等式 d(x,z)≤d(x,y)+d(y,z)。
- add_zero · prerequisite — 加法單位元：u+0=u。
- seq_limit_def · prerequisite — 數列極限：a_n→L 表示對每個 ε>0，存在 N 使所有 n≥N 都有 |a_n−L|<ε。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- mko_banach_def · cited — 實 Banach 空間必須把同一載體、實向量運算、範數、由該範數誘導的度量及完備性綁成一體。本輪使用有限維 ℝⁿ 配命名 ℓ¹ 或 ℓ^∞ 範數的精確定理證書，不以序列抽樣證完備。 · mko-real-banach-space
- mko_norm_def · cited — 範數把向量送到非負實數，且 norm(v)=0 當且僅當 v=0、norm(av)=|a| norm(v)、norm(u+v)≤norm(u)+norm(v)。 · mko-real-normed-vector-space
- mko_complete_def · cited — 度量空間 (X,d) 完備，若 X 內每個 Cauchy 序列都收斂到某個仍屬 X 的點；抽樣若干序列不足以證一般完備性。 · mko-complete-metric-space
- cauchy_def · prerequisite — 在度量空間 (X,d) 中，序列 (x^{(m)}) 是 Cauchy 序列，若對每個 ε>0 存在 N 使所有 m,p≥N 有 d(x^{(m)},x^{(p)})<ε；它收斂到 a，若對每個 ε>0 存在 N 使所有 m≥N 有 d(x^{(m)},a)<ε。
- real_cauchy_complete · prerequisite — 實數的 Cauchy 完備性：ℝ 中（以 |s−t| 為距離）每個 Cauchy 序列都收斂到某個實數。這是最小上界公理的標準推論，本稿不重證。
- inner_product_def · prerequisite — 實內積 ⟨·,·⟩ 是兩槽線性、對稱、正定的實值函數；範數由它誘導，指 ‖x‖²=⟨x,x⟩ 對所有 x 成立。
- thm_findim_complete · cited — 每個有限維實賦範向量空間，在由其範數誘導的度量下都是完備的；特別地，對每個正整數 n，(ℝⁿ,‖·‖₁) 與 (ℝⁿ,‖·‖_∞) 都是實 Banach 空間。 · Theo Buehler and Dietmar A. Salamon, Functional Analysis, 11 May 2016 notes, Corollary 1.2.7, p.16
- L_induced_metric · lemma — 若 ‖·‖ 是實向量空間 V 上的範數，則 d(x,y)=‖x−y‖ 是 V 上的度量。
- L_coord_le · lemma — 對 x,y∈ℝ² 與 k=1,2：|x_k−y_k|≤d₁(x,y)。
- L_parallelogram · lemma — 若範數由實內積誘導，則對所有 u,v：‖u+v‖²+‖u−v‖²=2‖u‖²+2‖v‖²。





## 逐步主鏈

S01 · definition操作前

(\mathbb{R}^2,\|\cdot\|_1)\ \text{Banach}

操作後

\|\cdot\|_1\ \text{norm}\ \land\ d_1=\|x-y\|_1\ \text{metric}\ \land\ (\mathbb{R}^2,d_1)\ \text{complete}

條件：無

規則：mko_banach_def · 依賴：G1, G2, mko_banach_def

葉節點依據：mko_banach_def + def_unfold

依 MKO，Banach 結構把同一個載體 ℝ²、它的向量運算、範數 ‖·‖₁、由這個範數誘導的度量 d₁ 與完備性綁在一起。所以要證三件事：‖·‖₁ 是範數（S02 到 S05）、d₁ 是度量（S06）、(ℝ²,d₁) 完備（S08 到 S12）。



S02 · equivalent操作前

\|x\|_1=|x_1|+|x_2|=0

操作後

x=(0,0);\ \ \text{and}\ \|x\|_1\ge 0\ \text{for all}\ x

條件：無

規則：abs_rules · 依賴：G2, abs_rules

葉節點依據：abs_rules + order_basics

|x₁|≥0、|x₂|≥0，所以和 ≥0。兩個非負數的和為 0 當且僅當兩者都為 0（若其一為正，和就為正），而 |t|=0 當且僅當 t=0，所以 ‖x‖₁=0 ⇔ x₁=x₂=0 ⇔ x=0。



S03 · equivalent操作前

\|\lambda x\|_1=|\lambda x_1|+|\lambda x_2|

操作後

\|\lambda x\|_1=|\lambda|(|x_1|+|x_2|)=|\lambda|\,\|x\|_1

條件：無

規則：abs_rules · 依賴：G1, G2, abs_rules

葉節點依據：abs_rules + distributive

λx 的坐標是 λx₁、λx₂（G1）。依 |uv|=|u||v| 得 |λx_k|=|λ||x_k|，再用分配律提出 |λ|。對每個實數 λ 與每個 x 成立。



S04 · implies操作前

\|x+y\|_1=|x_1+y_1|+|x_2+y_2|

操作後

\|x+y\|_1\le(|x_1|+|y_1|)+(|x_2|+|y_2|)=\|x\|_1+\|y\|_1

條件：無

規則：abs_rules · 依賴：G1, G2, abs_rules

葉節點依據：abs_rules + order_basics + add_assoc + add_comm

對每個坐標用實數三角不等式 |x_k+y_k|≤|x_k|+|y_k|，兩個不等式相加（順序公理允許同向不等式相加），再重新分組得 ‖x‖₁+‖y‖₁。



S05 · implies操作前

\text{S02},\ \text{S03},\ \text{S04}

操作後

(\mathbb{R}^2,\|\cdot\|_1)\ \text{is a real normed vector space}

條件：無

規則：mko_norm_def · 依賴：S02, S03, S04, mko_norm_def

葉節點依據：mko_norm_def + and_intro_elim

非負與正定（S02）、齊次（S03）、三角不等式（S04）正是 MKO 範數定義的三項，所以 ‖·‖₁ 是 ℝ² 上的範數。



S06 · theorem_application操作前

d_1(x,y)=\|x-y\|_1

操作後

d_1\ \text{is a metric on}\ \mathbb{R}^2

條件：無

規則：L_induced_metric · 依賴：S05, G2

葉節點依據：metric_def + mko_norm_def

依引理 L_induced_metric（任一範數誘導的 d(x,y)=‖x−y‖ 是度量），d₁ 是度量。引理在子步 S06.1 到 S06.3 只用 S02 到 S04 的三項範數公理證明。



S07 · implies操作前

x=(3,-1),\ y=(1,2)

操作後

d_1(x,y)=|2|+|-3|=5;\ \ \max(|2|,|-3|)=3\neq 5

條件：無

規則：numeric_evaluation · 依賴：G2, G3

葉節點依據：numeric_evaluation + abs_rules

x−y=(2,−3)，d₁(x,y)=2+3=5。對照：ℓ^∞ 範數給 max(2,3)=3。兩個數不同，說明 ℓ^∞ 度量不是 ‖·‖₁ 誘導的度量；MKO 要求 norm 與 metric 不可來自不同公式。



S08 · implies操作前

x,y\in\mathbb{R}^2,\ k\in\{1,2\}

操作後

|x_k-y_k|\le d_1(x,y)

條件：無

規則：L_coord_le · 依賴：G2

葉節點依據：abs_rules + order_basics

完備性證明的關鍵引理：每個坐標的距離都不超過 d₁ 距離（引理 L_coord_le）。證明在子步 S08.1。



S09 · implies操作前

(x^{(m)})\ \text{Cauchy in}\ (\mathbb{R}^2,d_1)

操作後

(x^{(m)}_k)_{m\ge1}\ \text{Cauchy in}\ \mathbb{R}\ \ (k=1,2)

條件：無

規則：cauchy_def · 依賴：S08, cauchy_def

葉節點依據：cauchy_def + L_coord_le + order_basics

取任意一個 d₁-Cauchy 序列（不指定具體數值）。給定 ε>0，由 Cauchy 定義取 N，使 m,p≥N 時 d₁(x^{(m)},x^{(p)})<ε；依 L_coord_le，|x^{(m)}_k−x^{(p)}_k|≤d₁(x^{(m)},x^{(p)})<ε。同一個 N 適用於兩個坐標，所以每個坐標序列都是實數 Cauchy 序列。



S10 · theorem_application操作前

(x^{(m)}_k)_{m\ge1}\ \text{Cauchy in}\ \mathbb{R}

操作後

x^{(m)}_k\to a_k\in\mathbb{R}\ (k=1,2),\ \ a=(a_1,a_2)\in\mathbb{R}^2

條件：無

規則：real_cauchy_complete · 依賴：S09, real_cauchy_complete

葉節點依據：real_cauchy_complete

依實數的 Cauchy 完備性，兩個坐標序列各自收斂到某個實數 a₁、a₂。令 a=(a₁,a₂)；a 是 ℝ² 的點，所以候選極限仍在空間內。這是本稿唯一從外部引入的分析事實。



S11 · implies操作前

x^{(m)}_1\to a_1,\ x^{(m)}_2\to a_2

操作後

d_1(x^{(m)},a)\to 0

條件：無

規則：cauchy_def · 依賴：S10, cauchy_def, G2

葉節點依據：cauchy_def + seq_limit_def + abs_rules

要證 x^{(m)} 在 d₁ 下收斂到 a。d₁(x^{(m)},a) 是兩個坐標誤差之和，所以讓每個誤差小於 ε/2 即可。子步 S11.1 選出共同門檻，S11.2 完成估計。



S12 · implies操作前

\text{arbitrary Cauchy}\ (x^{(m)})\ \text{converges in}\ (\mathbb{R}^2,d_1)

操作後

(\mathbb{R}^2,d_1)\ \text{complete};\ (\mathbb{R}^2,\|\cdot\|_1)\ \text{real Banach space}

條件：無

規則：forall_intro · 依賴：S05, S06, S09, S10, S11, mko_complete_def, mko_banach_def

葉節點依據：forall_intro + mko_complete_def + mko_banach_def

S09 到 S11 對任意 d₁-Cauchy 序列成立，所以依全稱引入，每個 Cauchy 序列都收斂到 ℝ² 中的點：(ℝ²,d₁) 完備。加上 S05 的範數與 S06 的誘導度量，三項都綁定同一結構，依 MKO，(ℝ²,‖·‖₁) 是實 Banach 空間。



S13 · theorem_application操作前

\dim\mathbb{R}^n=n<\infty,\ \ \|\cdot\|\in\{\|\cdot\|_1,\|\cdot\|_\infty\}

操作後

(\mathbb{R}^n,\|\cdot\|)\ \text{Banach (named-theorem certificate)}

條件：n\ \text{finite}

規則：thm_findim_complete · 依賴：S12, thm_findim_complete

葉節點依據：thm_findim_complete

MKO 的證書形式是命名定理：每個有限維實賦範空間在其誘導度量下完備。前提是有限維與「度量由同一範數誘導」。S08 到 S12 是這個定理在 n=2、ℓ¹ 時的完整證明，只依賴實數完備性；ℓ^∞ 與一般 n 的情形本稿只引用，不另證（同樣的坐標論證也可行，但未寫出）。



S14 · implies操作前

u=(1,0),\ v=(0,1):\ \|u+v\|_1^2+\|u-v\|_1^2=2^2+2^2=8

操作後

8\neq 4=2\|u\|_1^2+2\|v\|_1^2\ \Rightarrow\ \|\cdot\|_1\ \text{induced by no inner product}

條件：無

規則：L_parallelogram · 依賴：G3, S12

葉節點依據：contrapositive + numeric_evaluation

u+v=(1,1)、u−v=(1,−1)，ℓ¹ 範數都是 2，所以左邊 4+4=8；而 ‖u‖₁=‖v‖₁=1，右邊 2+2=4。依引理 L_parallelogram 的逆否命題，‖·‖₁ 不是由任何內積誘導。MKO 指出：Banach 的指定範數不自動由內積誘導，也不自動成為相容的 Hilbert 結構；不否認底層向量空間另有內積。引理在子步 S14.1、S14.2 證明。



S15 · implies操作前

\text{S06},\ \text{S07},\ \text{S12},\ \text{S14}

操作後

(\mathbb{R}^2,\|\cdot\|_1)\ \text{Banach};\ d_1((3,-1),(1,2))=5;\ \|\cdot\|_1\ \text{not from an inner product}

條件：無

規則：and_intro_elim · 依賴：S06, S07, S12, S13, S14

葉節點依據：and_intro_elim

合併：‖·‖₁ 是範數，d₁ 是它誘導的度量，d₁((3,−1),(1,2))=5；(ℝ²,d₁) 完備，所以是實 Banach 空間；ℓ¹ 範數違反平行四邊形律，不來自內積。







## 局部子步與引理

S06.1 · equivalent操作前

d(x,y)=\|x-y\|

操作後

d(x,y)\ge 0,\ \ d(x,y)=0\iff x-y=0\iff x=y

條件：無

規則：mko_norm_def · 依賴：S02

葉節點依據：mko_norm_def + vector_space_axioms

範數非負，所以 d≥0；範數為 0 當且僅當向量為 0，而 x−y=0 當且僅當 x=y（兩邊加 y）。



S06.2 · equivalent操作前

d(y,x)=\|y-x\|=\|(-1)(x-y)\|

操作後

d(y,x)=|-1|\,\|x-y\|=d(x,y)

條件：無

規則：mko_norm_def · 依賴：S03

葉節點依據：mko_norm_def + vector_space_axioms + abs_rules

y−x=(−1)(x−y)（向量空間公理），由齊次性 ‖(−1)z‖=|−1|‖z‖=‖z‖，所以 d 對稱。



S06.3 · implies操作前

x-z=(x-y)+(y-z)

操作後

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

條件：無

規則：mko_norm_def · 依賴：S04

葉節點依據：mko_norm_def + vector_space_axioms + metric_def

把 x−z 拆成 (x−y)+(y−z)，再用範數三角不等式。S06.1 到 S06.3 合起來證得引理 L_induced_metric：非負與分離、對稱、三角不等式都成立。



S08.1 · implies操作前

d_1(x,y)=|x_1-y_1|+|x_2-y_2|

操作後

d_1(x,y)\ge|x_1-y_1|\ \text{and}\ d_1(x,y)\ge|x_2-y_2|

條件：無

規則：order_basics · 依賴：G2, abs_rules

葉節點依據：abs_rules + order_basics + add_zero

因 |x₂−y₂|≥0，d₁(x,y)=|x₁−y₁|+|x₂−y₂|≥|x₁−y₁|+0；同理把第一項換成 0 得第二個不等式。這證得引理 L_coord_le。



S11.1 · implies操作前

\varepsilon>0;\ \exists N_k:\ m\ge N_k\Rightarrow|x^{(m)}_k-a_k|<\tfrac{\varepsilon}{2}

操作後

N=\max(N_1,N_2):\ m\ge N\Rightarrow|x^{(m)}_1-a_1|<\tfrac{\varepsilon}{2}\ \land\ |x^{(m)}_2-a_2|<\tfrac{\varepsilon}{2}

條件：\varepsilon>0

規則：seq_limit_def · 依賴：S10, seq_limit_def

葉節點依據：seq_limit_def + order_basics

給定 ε>0，則 ε/2>0；依實數列極限定義，對每個 k 有 N_k 使 m≥N_k 時坐標誤差小於 ε/2。取 N=max(N₁,N₂)，則 m≥N 同時蘊含 m≥N₁ 與 m≥N₂。



S11.2 · implies操作前

m\ge N

操作後

d_1(x^{(m)},a)=|x^{(m)}_1-a_1|+|x^{(m)}_2-a_2|<\tfrac{\varepsilon}{2}+\tfrac{\varepsilon}{2}=\varepsilon

條件：無

規則：order_basics · 依賴：S11.1, G2

葉節點依據：order_basics + frac_rules + cauchy_def

兩個嚴格不等式相加得和小於 ε/2+ε/2=ε（N7 核對這個代數恆等式）。ε 是任意正數，依收斂定義 x^{(m)}→a。



S14.1 · equivalent操作前

\langle u\pm v,u\pm v\rangle

操作後

\langle u,u\rangle\pm 2\langle u,v\rangle+\langle v,v\rangle

條件：無

規則：inner_product_def · 依賴：inner_product_def

葉節點依據：inner_product_def + distributive

用兩槽線性展開：⟨u±v,u±v⟩=⟨u,u⟩±⟨u,v⟩±⟨v,u⟩+⟨v,v⟩；再用對稱性 ⟨v,u⟩=⟨u,v⟩ 合併中間兩項。



S14.2 · equivalent操作前

\langle u+v,u+v\rangle+\langle u-v,u-v\rangle

操作後

2\langle u,u\rangle+2\langle v,v\rangle,\ \text{i.e.}\ \|u+v\|^2+\|u-v\|^2=2\|u\|^2+2\|v\|^2

條件：無

規則：eq_replace · 依賴：S14.1

葉節點依據：eq_replace + add_inverse + inner_product_def

把 S14.1 的兩式相加，±2⟨u,v⟩ 互相抵消；再用 ‖z‖²=⟨z,z⟩ 改寫成範數。S14.1 與 S14.2 合起來證得引理 L_parallelogram。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S06, S07, S12, S14, and_intro_elim — 目標是三個任務的合取；各部分由所列步驟正向證得，H⇒G 由合取引入。
- S14.2 · inverse_equivalence · S14.1, add_inverse, inner_product_def — 相加與改寫都是等值操作，雙向成立。
- S14.1 · inverse_equivalence · inner_product_def — 展開是恆等式，兩邊同值。
- S14 · premise_audit · L_parallelogram, contrapositive, numeric_evaluation — 只用引理的必要方向（內積範數 ⇒ 平行四邊形律）；一組反例足以否定（N5、N6）。
- S13 · premise_audit · thm_findim_complete, S12 — 定理的引用帶 citation_verified；有限維是必要的前提，無限維賦範空間可以不完備（見錯誤控制）。
- S12 · sufficient_goal_reduction · S05, S06, S11, forall_intro, mko_complete_def, mko_banach_def — 目標 G：Banach。足夠條件 H：範數、同一範數誘導的度量、完備；H⇒G 由 MKO 定義。H 由 S05、S06 與 S09 到 S11 正向證得，沒有用到 G，也沒有用到任何序列樣本。
- S11.2 · premise_audit · S11.1, order_basics, cauchy_def — 用到同向嚴格不等式可相加；ε 未被指定，所以結論對每個 ε 成立。
- S11.1 · premise_audit · seq_limit_def, order_basics — 需要 ε/2>0（正數除以 2 仍為正）與最大值的性質；只有兩個坐標，所以 max 有限。
- S11 · premise_audit · S10, cauchy_def — 需要兩個坐標都收斂；只有一個坐標收斂不足以推出 d₁ 收斂。
- S10 · premise_audit · S09, real_cauchy_complete — 前提是坐標序列為 Cauchy（S09）；real_cauchy_complete 是前置規則，未在本稿證明，見待處理項。
- S09 · premise_audit · S08, cauchy_def, order_basics — 用到 ≤ 與 < 的傳遞性；序列是任意的，S12 才能全稱化。
- S08.1 · premise_audit · abs_rules, order_basics — 只用 |t|≥0 與「u≥0 ⇒ s+u≥s」。
- S08 · premise_audit · L_coord_le — 只宣稱一個方向的不等式；坐標距離小並不推出 d₁ 小，除非兩個坐標都小（S11 處理）。
- S07 · premise_audit · G2, numeric_evaluation — 精確計算（N1、N2）；只說明這兩個度量不同，不推出任何完備性結論。
- S06.3 · premise_audit · mko_norm_def, vector_space_axioms — 只需範數三角不等式與向量加法的結合律；不宣稱反向。
- S06.2 · inverse_equivalence · mko_norm_def, vector_space_axioms, abs_rules — 等式鏈每一步都是等值改寫，雙向成立。
- S06.1 · inverse_equivalence · mko_norm_def, vector_space_axioms — 每個 ⇔ 都由範數公理或向量加法的可逆性給出，雙向成立。
- S06 · premise_audit · S05, L_induced_metric — 需要 ‖·‖₁ 是範數（S05）；反向（每個度量都來自範數）不成立，見負向控制。
- S05 · sufficient_goal_reduction · S02, S03, S04, mko_norm_def — 目標：‖·‖₁ 是範數。足夠條件：三項公理；三項都已正向證得，沒有把目標當作前提。
- S04 · premise_audit · abs_rules, order_basics, add_assoc, add_comm — 這是不等式，只有一個方向；等號何時成立不在本稿宣稱範圍內。N4 是有限格點核對，不是證明。
- S03 · inverse_equivalence · abs_rules, distributive — 所用都是恆等式，兩邊同值；N3 在一個整數格上作有限核對，只是輔助。
- S02 · inverse_equivalence · abs_rules, order_basics — 反向：x=(0,0) 時 |0|+|0|=0。正向用「非負數之和為 0 ⇒ 各項為 0」，由順序公理得到。
- S01 · premise_audit · mko_banach_def, G2 — 只展開定義；G2 固定度量必須來自同一範數，S07 的 ℓ^∞ 對照說明換了度量就不是同一結構。





## 錯誤控制與反例

抽樣 Cauchy 序列不證完備MKO 指出的誤解是測過幾條 Cauchy 序列就宣稱 Banach。完備性量化所有 Cauchy 序列。反例：有限支撐實數列空間 c₀₀ 配 ℓ¹ 範數，序列 x^{(m)} 的第 k 項在 k≤m 時為 2^{−k}、k>m 時為 0；它是 Cauchy（m<p 時距離 Σ_{k=m+1}^{p} 2^{−k}<2^{−m}），但若有極限 y，坐標必為 y_k=2^{−k}，不是有限支撐，所以 c₀₀ 不完備。在 c₀₀ 中抽到的許多 Cauchy 序列（例如最終為常數的）都收斂，只抽到這些收斂例子不保證揭露缺陷；若選到上述 x^{(m)} 並完整證明它是 Cauchy 且在 c₀₀ 中無極限，就能揭露不完備。有限多個截斷值本身仍不是那個完整證明。本稿的完備性來自 S09 到 S12 對任意序列的證明。

度量必須由同一範數誘導MKO 的另一個誤解是只知道 metric 完備就宣稱 Banach。d′(x,y)=min(1,‖x−y‖₁) 是 ℝ² 上的完備度量，但不由任何範數誘導：若 d′(x,y)=‖x−y‖ 對某範數成立，則 d′(2e₁,0)=2d′(e₁,0)；實際上左邊 min(1,2)=1，右邊 2·min(1,1)=2。同樣，S07 顯示 ℓ^∞ 度量不是 ‖·‖₁ 誘導的度量。

Banach 空間不一定是 Hilbert 空間完備的賦範空間不一定有能誘導其指定範數的內積；這不否認底層向量空間可另配不相容的內積，例如 ℝ² 的標準點積。S14 證明 ℓ¹ 範數違反平行四邊形律（8≠4），所以 (ℝ²,‖·‖₁) 是 Banach 空間，但它的範數不來自內積。


- 在 (ℝ²,‖·‖₁) 中測了五條 Cauchy 序列都收斂，所以它完備 → reject — 結論雖真，但有限抽樣不是證明；c₀₀ 中抽樣也能全部收斂卻不完備。完備性來自 S09 到 S12。
- (ℝ²,‖·‖₁) 配上 ℓ^∞ 度量就是這個 Banach 空間 → reject — ℓ^∞ 度量不由 ‖·‖₁ 誘導：(3,−1) 與 (1,2) 的距離是 3，而 ‖x−y‖₁=5。
- d′(x,y)=min(1,‖x−y‖₁) 是 ℝ² 上的完備度量，所以 (ℝ²,d′) 是 Banach 空間 → reject — d′ 不由範數誘導：d′(2e₁,0)=1，而齊次性要求 2d′(e₁,0)=2。
- 每個 Banach 空間的範數都由某個內積誘導 → reject — ℓ¹ 範數在 u=(1,0)、v=(0,1) 違反平行四邊形律：8≠4。





## 結論與限制

‖x‖₁=|x₁|+|x₂| 是 ℝ² 上的範數，d₁(x,y)=‖x−y‖₁ 是它誘導的度量，d₁((3,−1),(1,2))=5（ℓ^∞ 度量給 3，是不同的度量）。任意 d₁-Cauchy 序列的坐標都是實數 Cauchy 序列，收斂到 a₁、a₂，且 d₁(x^{(m)},a)→0，所以 (ℝ²,‖·‖₁) 是實 Banach 空間；一般有限維情形由命名定理給出（citation_verified）。ℓ¹ 範數在 u=(1,0)、v=(0,1) 違反平行四邊形律（8≠4），所以不由任何內積誘導。


- 實數的 Cauchy 完備性（real_cauchy_complete）是前置規則，本稿不由最小上界公理重新推導。
- 錯誤控制中 d′=min(1,‖x−y‖₁) 是完備度量、c₀₀ 不完備兩件事只以簡述說明，未寫成完整步驟。
- N3、N4 是整數格點上的有限核對，只是輔助；S03、S04 的一般結論由絕對值規則證明。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 6d484742c41cc5faf58a8fd96615e0ff74a6ce36d276c7cac9e25d827f7c0e8a
- original source SHA-256: 623ecd0be3adc5a95eedf871819e318c00b6c2f08da1df036992524ab9710438
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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