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

目標與範圍

在 ℝ² 中令 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。

逐步主鏈

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

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

\lambda_1,\lambda_2,\lambda_3\ge0

\tfrac16+\tfrac13+\tfrac12

1

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

(2,3)=w

\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

\tfrac12v_1+\tfrac12v_2+0\cdot v_3

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

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

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

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

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

\lambda_1=-\tfrac13<0

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

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

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

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

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

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

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)

\text{S05 to S13}

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

局部子步與引理

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

2

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

3

\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

\lambda_1+\tfrac23+\tfrac23=1

\lambda_1=-\tfrac13

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

\sum_i\lambda_i\ell(v_i)

\sum_i\lambda_i\ell(v_i)

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

逐步反向審查

• 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 的上界獨立確認。

近似和不等於精確 1

MKO 的另一個誤解是把 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、反控制與修訂記錄）