# 有限凸組合：以精確權重核對見證，並區分負權重、近似權重與唯一性

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

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

derivation-mko-finite-convex-combination-01 · production-20261019-adopted-96



## 目標與範圍

在 ℝ² 中令 v_1=(0,0)、v_2=(6,0)、v_3=(0,6)。(1) 核對 λ=(1/6,1/3,1/2) 是凸權重並重建 w=(2,3)；(2) 說明零權重允許、兩點凸組合是線段點；(3) 證明 u=(4,4) 不是 v_1、v_2、v_3 的凸組合（唯一的仿射權重含 −1/3），並以線性泛函上界給第二個證明；(4) 說明 0.333 三個權重不合格；(5) 加入 v_4=(3,3) 後，同一點有兩組不同的凸權重。

只處理 G1 到 G3 的整數座標向量與精確有理權重（MKO 假設 a1）。凸組合見證只證給定加權點，不主張座標唯一（a2）。凸集合、凸包與仿射獨立的一般理論不在範圍內。不改動 canonical MKO 或其英文 edition。





## 已知條件與符號


- vector_space_axioms
- finite_sum_rules
- order_basics
- cartesian_product_def
- numeric_evaluation


- G1 — ℝ² 中 v_1=(0,0)、v_2=(6,0)、v_3=(0,6)；權重為精確有理數，不接受浮點近似（MKO 假設 a1）。
- G2 — 候選見證：w=(2,3)，λ=(1/6,1/3,1/2)。
- G3 — 其他資料：點 (3,0) 配權重 (1/2,1/2,0)；u=(4,4)；十進位權重 (0.333,0.333,0.333)；第四點 v_4=(3,3)。


- v_1=(0,0),\ v_2=(6,0),\ v_3=(0,6) — 給定的三個點
- v_4=(3,3) — 加入的第四個點
- \lambda=(\lambda_1,\lambda_2,\lambda_3) — 權重
- w=(2,3),\ u=(4,4) — 目標點與反例點
- \ell(x,y)=x+y — 用於上界論證的線性泛函





## 規則與來源


- vector_space_axioms · prerequisite — 向量空間公理（實數或其他域 F 上）：加法成交換群；純量乘法滿足 a(u+v)=au+av、(a+b)u=au+bu、(ab)u=a(bu)、1u=u。
- finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。
- 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。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- 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）。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- mko_convex_def · cited — 向量 v_1 到 v_n 的有限凸組合為 Σ λ_i v_i，其中 n≥1、每個 λ_i≥0 且 Σ λ_i=1。零權重允許；負權重或只近似和為 1 只形成一般仿射或線性組合。 · mko-finite-convex-combination
- p_affine_comb · prerequisite — 仿射組合：Σ λ_i v_i 且 Σ λ_i=1，權重符號不限；線性組合：權重沒有任何限制。
- L_bound · lemma — 設 ℓ(x,y)=αx+βy，λ_i≥0、Σλ_i=1，且對每個 i 有 ℓ(v_i)≤M。則 ℓ(Σλ_i v_i)≤M。





## 逐步主鏈

S01 · definition操作前

w\ \text{convex combination of}\ v_1,v_2,v_3

操作後

\exists\lambda:\ \lambda_i\ge0,\ \sum_i\lambda_i=1,\ \sum_i\lambda_iv_i=w

條件：n=3\ge1

規則：mko_convex_def · 依賴：mko_convex_def

葉節點依據：mko_convex_def + def_unfold

依 MKO 展開：凸組合需要三件事分別成立：每個權重非負、權重和精確為 1、加權和等於目標（MKO 段落 0、2）。見證就是一組滿足三件事的權重。



S02 · implies操作前

\lambda=(\tfrac16,\tfrac13,\tfrac12)

操作後

\lambda_1,\lambda_2,\lambda_3\ge0

條件：無

規則：order_basics · 依賴：G2, S01

葉節點依據：order_basics

三個權重都是正有理數，所以非負。這是第一個條件。



S03 · equivalent操作前

\tfrac16+\tfrac13+\tfrac12

操作後

1

條件：無

規則：numeric_evaluation · 依賴：G2, S01

葉節點依據：numeric_evaluation + frac_rules

通分：1/6+2/6+3/6=6/6=1（N1），是精確等式。這是第二個條件。



S04 · equivalent操作前

\tfrac16(0,0)+\tfrac13(6,0)+\tfrac12(0,6)

操作後

(2,3)=w

條件：無

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

葉節點依據：vector_space_axioms + cartesian_product_def

逐坐標重建（S04.1、S04.2）：第一坐標 2、第二坐標 3，正是 w。這是第三個條件，也是 MKO 段落 2 所說的「以精確重建目標核對」。



S05 · implies操作前

\lambda_i\ge0,\ \sum\lambda_i=1,\ \sum\lambda_iv_i=w

操作後

w=(2,3)\ \text{is a convex combination of}\ v_1,v_2,v_3

條件：無

規則：exists_intro · 依賴：S02, S03, S04, S01

葉節點依據：exists_intro + and_intro_elim

三個條件都通過，λ=(1/6,1/3,1/2) 是見證，依 ∃引入得 w 是凸組合。見證只證明這個點是凸組合，不說明權重唯一（MKO 假設 a2）。



S06 · implies操作前

\tfrac12v_1+\tfrac12v_2+0\cdot v_3

操作後

(3,0)\ \text{with weights}\ (\tfrac12,\tfrac12,0)\ \text{convex}

條件：\lambda_3=0

規則：mko_convex_def · 依賴：G3, S01

葉節點依據：mko_convex_def + numeric_evaluation

權重 1/2、1/2、0 都非負（0 也是非負），和為 1（N5）；重建：第一坐標 1/2·6=3（N4），第二坐標 0。所以 (3,0) 是凸組合；零權重是允許的，它只是讓 v_3 不起作用。



S07 · implies操作前

\lambda v_2+(1-\lambda)v_3,\ \lambda\in[0,1]

操作後

(6\lambda,\ 6-6\lambda);\ \lambda=\tfrac13:\ (2,4)

條件：0\le\lambda\le1

規則：vector_space_axioms · 依賴：G1, S01, vector_space_axioms

葉節點依據：vector_space_axioms + order_basics + distributive

兩點凸組合用 λ 與 1−λ（MKO 段落 1）：兩者都非負若且唯若 0≤λ≤1，和自動為 1。坐標為 (6λ, 6−6λ)（N6、N7 為恆等式），λ 從 0 到 1 走過從 v_3 到 v_2 的線段。λ=1/3 給 (2,4)（N8、N9）。



S08 · equivalent操作前

\sum_i\lambda_i=1,\ \sum_i\lambda_iv_i=(4,4)

操作後

\lambda=(-\tfrac13,\ \tfrac23,\ \tfrac23)\ \text{(the only solution)}

條件：無

規則：eq_congruence · 依賴：G1, G3, p_affine_comb

葉節點依據：eq_congruence + mul_inverse_nonzero

設任意權重和為 1 且加權和為 u=(4,4)。因 v_1=(0,0)，第一坐標給 6λ_2=4、第二坐標給 6λ_3=4（S08.1），所以 λ_2=λ_3=2/3；和為 1 給 λ_1=1−4/3=−1/3（S08.2）。每一步都是等價變形，所以這是唯一的仿射權重。



S09 · implies操作前

\lambda_1=-\tfrac13<0

操作後

u=(4,4)\ \text{affine but not a convex combination of}\ v_1,v_2,v_3

條件：無

規則：contradiction · 依賴：S08, S01, p_affine_comb

葉節點依據：contradiction + order_basics

若 u 是凸組合，其凸權重也是和為 1 的權重，由 S08 必為 (−1/3,2/3,2/3)，但 −1/3<0（N12）違反非負性，矛盾。所以 u 不是凸組合；它只是仿射組合（MKO：負權重只形成一般仿射組合）。



S10 · theorem_application操作前

\lambda_i\ge0,\ \sum\lambda_i=1,\ \ell(v_i)\le M

操作後

\ell\Big(\sum_i\lambda_iv_i\Big)\le M

條件：無

規則：L_bound · 依賴：L_bound

葉節點依據：L_bound + vector_space_axioms

引理 L_bound（S10.1、S10.2 證明）：凸組合在線性泛函下的值不超過各點值的上界。這給出不依賴解方程的第二種排除方法，而且明顯用到權重非負。



S11 · implies操作前

\ell(x,y)=x+y:\ \ell(v_1)=0,\ \ell(v_2)=6,\ \ell(v_3)=6

操作後

\ell(u)=8>6\ \Rightarrow\ u\ \text{not a convex combination}

條件：無

規則：contrapositive · 依賴：S10, G1, G3

葉節點依據：contrapositive + L_bound + numeric_evaluation

取 ℓ(x,y)=x+y，三點的值為 0、6、6，所以 M=6。若 u 是凸組合，L_bound 給 ℓ(u)≤6，但 ℓ(u)=4+4=8>6（N14、N15）。由逆否，u 不是凸組合，與 S09 一致。仿射權重 (−1/3,2/3,2/3) 給 −1/3·0+2/3·6+2/3·6=8，正是負權重讓值越過上界。



S12 · implies操作前

\lambda=(0.333,\ 0.333,\ 0.333)

操作後

\sum\lambda_i=0.999\neq1:\ \text{not convex weights}

條件：無

規則：numeric_evaluation · 依賴：G3, S01, G1

葉節點依據：numeric_evaluation + frac_rules

0.333 是精確的有理數 333/1000，三個相加為 0.999（N16），不等於 1（N17），總和條件失敗，所以不是凸權重；加權和 (1.998, 1.998) 也不是 (2,2)。精確權重 (1/3,1/3,1/3) 和為 1（N18），給出 (2,2)，才是合格見證。MKO 假設 a1 不接受浮點近似。



S13 · implies操作前

v_4=(3,3)

操作後

(3,3)=1\cdot v_4=\tfrac12v_2+\tfrac12v_3:\ \text{weights}\ (0,0,0,1)\ \text{and}\ (0,\tfrac12,\tfrac12,0)

條件：無

規則：mko_convex_def · 依賴：G3, S01, G1

葉節點依據：mko_convex_def + numeric_evaluation

在四點 v_1、v_2、v_3、v_4 上，(3,3) 有兩組凸權重：(0,0,0,1) 直接取 v_4；(0,1/2,1/2,0) 給 (1/2·6, 1/2·6)=(3,3)（N19、N20）。兩組都非負、和為 1，但不同。所以凸組合見證不帶來座標唯一性；仿射獨立可保證整個族上凸表示的唯一性，但不是個別點唯一表示的必要條件；此處 v_4 在 v_2、v_3 的線段上，已明示 (3,3) 不唯一，不能把這個結論外推成每個點都不唯一。



S14 · implies操作前

\text{S05 to S13}

操作後

\text{convex}\iff(\lambda_i\ge0)\land(\textstyle\sum\lambda_i=1)\land(\text{exact reconstruction})

條件：無

規則：and_intro_elim · 依賴：S05, S06, S09, S11, S12, S13

葉節點依據：and_intro_elim

總結：w=(2,3) 以 (1/6,1/3,1/2) 為見證；零權重允許；u=(4,4) 的唯一仿射權重含負數，且 x+y=8>6，不是凸組合；0.333 三個權重和為 0.999，不合格；凸權重可以不唯一。







## 局部子步與引理

S04.1 · equivalent操作前

\tfrac16\cdot0+\tfrac13\cdot6+\tfrac12\cdot0

操作後

2

條件：無

規則：numeric_evaluation · 依賴：G1, G2

葉節點依據：numeric_evaluation + mul_zero

第一坐標：只有 v_2 的第一坐標非零，1/3·6=2（N2）。



S04.2 · equivalent操作前

\tfrac16\cdot0+\tfrac13\cdot0+\tfrac12\cdot6

操作後

3

條件：無

規則：numeric_evaluation · 依賴：G1, G2

葉節點依據：numeric_evaluation + mul_zero

第二坐標：只有 v_3 的第二坐標非零，1/2·6=3（N3）。



S08.1 · equivalent操作前

\lambda_1(0,0)+\lambda_2(6,0)+\lambda_3(0,6)=(4,4)

操作後

6\lambda_2=4,\ 6\lambda_3=4\ \Longleftrightarrow\ \lambda_2=\lambda_3=\tfrac23

條件：6\neq0

規則：cartesian_product_def · 依賴：G1, cartesian_product_def

葉節點依據：cartesian_product_def + mul_inverse_nonzero

加權和為 (6λ_2, 6λ_3)，與 (4,4) 逐坐標相等。兩邊乘 1/6 得 λ_2=λ_3=4/6=2/3（N10）。λ_1 不出現在坐標方程中，因為 v_1 是原點。



S08.2 · equivalent操作前

\lambda_1+\tfrac23+\tfrac23=1

操作後

\lambda_1=-\tfrac13

條件：無

規則：eq_congruence · 依賴：S08.1, eq_congruence

葉節點依據：eq_congruence + add_inverse + numeric_evaluation

兩邊同減 4/3：λ_1=1−4/3=−1/3（N11）。



S10.1 · equivalent操作前

\ell\Big(\sum_i\lambda_iv_i\Big)

操作後

\sum_i\lambda_i\ell(v_i)

條件：無

規則：distributive · 依賴：vector_space_axioms, distributive

葉節點依據：distributive + finite_sum_rules

寫 v_i=(x_i,y_i)。Σλ_iv_i=(Σλ_ix_i, Σλ_iy_i)，所以 ℓ 的值為 αΣλ_ix_i+βΣλ_iy_i=Σλ_i(αx_i+βy_i)=Σλ_iℓ(v_i)（分配律；N13 對三點、α=β=1 驗證恆等式）。



S10.2 · implies操作前

\sum_i\lambda_i\ell(v_i)

操作後

\le\sum_i\lambda_iM=M\sum_i\lambda_i=M

條件：\lambda_i\ge0; \sum_i\lambda_i=1

規則：order_basics · 依賴：S10.1, order_basics, finite_sum_rules

葉節點依據：order_basics + finite_sum_rules + mul_one

對每個 i，ℓ(v_i)≤M 且 λ_i≥0，乘以非負數保持 ≤：λ_iℓ(v_i)≤λ_iM。相加得 Σλ_iℓ(v_i)≤MΣλ_i=M。S10.1 與 S10.2 證得引理 L_bound。若某個 λ_i<0，乘法會反轉不等號，這一步就失效。







## 逐步反向審查


- S14 · premise_audit · S05, S09, S12, S13 — 只合取已證結論。
- S13 · premise_audit · mko_convex_def, numeric_evaluation — 兩組見證都完整核對三個條件；一個例子就否定「凸權重必唯一」。
- S12 · premise_audit · numeric_evaluation — 截斷小數是一個確定的有理數；無限循環的 0.9（9 循環）作為實數等於 1，但截斷後的 0.999 不等於 1。
- S11 · premise_audit · L_bound, contrapositive, numeric_evaluation — 上界論證只能排除，不能證明某點是凸組合；例如 (−1,1) 滿足 x+y=0≤6，卻不是凸組合：它的第一坐標為負，而每個凸組合的第一坐標都至少為 0。所以反向不成立。
- S10.2 · premise_audit · order_basics, finite_sum_rules — 只宣稱上界；兩個條件（非負、和為 1）都被用到。
- S10.1 · inverse_equivalence · distributive, finite_sum_rules — 恆等變形，雙向成立；這一步不需要權重非負。
- S10 · premise_audit · L_bound — 需要凸權重；仿射權重（可負）不滿足這個上界（S11）。
- S09 · premise_audit · S08, contradiction, order_basics — 關鍵是 S08 的唯一性：若仿射權重不唯一，一組負權重不足以排除凸組合。
- S08.2 · inverse_equivalence · eq_congruence, add_inverse — 減與加互逆。
- S08.1 · inverse_equivalence · cartesian_product_def, mul_inverse_nonzero — 有序對相等與乘非零數都可逆。
- S08 · inverse_equivalence · eq_congruence, mul_inverse_nonzero — 反向：代回 (−1/3,2/3,2/3) 得和 1、加權和 (4,4)；除以 6 需 6≠0。
- S07 · premise_audit · vector_space_axioms, order_basics — λ 在 [0,1] 外時 λ 或 1−λ 為負，得到的是直線上的仿射組合而不是線段上的凸組合。
- S06 · premise_audit · mko_convex_def, numeric_evaluation — 定義要求 λ_i≥0，不是 λ_i>0；三個條件都已核。
- S05 · premise_audit · S02, S03, S04, exists_intro — 存在性只需一組見證；唯一性另議（S13）。
- S04.2 · inverse_equivalence · numeric_evaluation — 精確求值。
- S04.1 · inverse_equivalence · numeric_evaluation — 精確求值。
- S04 · inverse_equivalence · vector_space_axioms, cartesian_product_def — 向量相等 ⇔ 兩個坐標都相等，雙向成立。
- S03 · inverse_equivalence · numeric_evaluation, frac_rules — 精確有理數求和，可獨立重算。
- S02 · premise_audit · order_basics — 逐一核對三個權重；非負性與總和為 1 是分開的條件。
- S01 · premise_audit · mko_convex_def — 只展開定義；三個條件缺一不可，之後逐一核對。





## 錯誤控制與反例

負權重只給仿射組合MKO 指出的誤解之一是允許負權重。u=(4,4) 可寫成 −1/3v_1+2/3v_2+2/3v_3，權重和為 1，但這只是仿射組合。S08 證明這是唯一的仿射權重，S09 因而排除凸組合；S11 用 x+y≤6 的上界獨立確認。

近似和不等於精確 1MKO 的另一個誤解是把 0.999 這類近似值當成精確的 1。三個 0.333 的和是 0.999，不是 1，所以不合格；正確的見證要用精確有理數 1/3。（無限循環的 9 作為實數等於 1，但題庫只用有限、精確的有理權重。）

見證不帶來唯一座標MKO 的第三個誤解是由凸組合直接聲稱唯一座標。S13 中 (3,3) 在 v_1 到 v_4 上有 (0,0,0,1) 與 (0,1/2,1/2,0) 兩組凸權重。唯一性須另作論證；仿射獨立是保證全族唯一性的充分條件，不是每個個別點唯一表示的必要條件；本稿在 S08 對三點 v_1、v_2、v_3 的仿射權重唯一性是直接解方程得到的，不是由見證推出的。


- 權重 (−1/3,2/3,2/3) 和為 1，所以 u=(4,4) 是 v_1、v_2、v_3 的凸組合 → reject — −1/3<0；而且這是唯一的仿射權重（S08、S09），x+y=8>6（S11）。
- (0.333,0.333,0.333) 是凸權重 → reject — 和為 0.999≠1（S12）。
- (3,3)=1·v_4，所以它在 v_1 到 v_4 上的凸座標唯一為 (0,0,0,1) → reject — (0,1/2,1/2,0) 也給出 (3,3)（S13）。
- 凸組合的權重必須全為正，所以 (3,0)=1/2v_1+1/2v_2+0v_3 不是凸組合 → reject — 定義只要求 λ_i≥0，零權重允許（S06）。





## 結論與限制

λ=(1/6,1/3,1/2) 非負、和為 1、重建 (2,3)，所以 w=(2,3) 是 v_1、v_2、v_3 的凸組合；(3,0)=1/2v_1+1/2v_2+0v_3 也是（零權重允許）；λv_2+(1−λ)v_3（0≤λ≤1）走過線段，λ=1/3 給 (2,4)。u=(4,4) 唯一的仿射權重是 (−1/3,2/3,2/3)，且 x+y=8 超過上界 6，故不是凸組合。(0.333,0.333,0.333) 和為 0.999，不合格。加入 v_4=(3,3) 後，(3,3) 有兩組不同的凸權重。


- 凸集合、凸包與仿射獨立的一般理論（MKO 的 formal next）不在範圍內；S08 的唯一性只對 v_1、v_2、v_3 直接解方程得到。
- S11 的上界論證只能排除點，不能證明一點是凸組合。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 883bd8ea9e8aa6424a1a57388935dbdcff2c47f965eba50f18d4f37366e19d03
- original source SHA-256: 0a525035a113a0483c2c6902ae703bbc991232a443c60a2cb924e27999cf2bad
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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




