凸集合：半空間與軸對齊盒的完整凸性證書，及有限點集的中點反例

目標與範圍

在實向量空間 ℝ² 中：（一）證明閉半空間 H={(x,y) ∣ 2x−3y≤6} 是凸集合；（二）證明非空軸對齊盒 B=[−1,2]×[0,3] 是凸集合；兩個證明都必須對所有 p、q 與所有 λ∈[0,1] 成立。（三）用一個精確的中點見證否證有限點集 F={(0,0),(2,0),(0,2)} 的凸性，並說明為何抽查有限個 λ、或找不到反例，都不能證明凸性。

停在 MKO 的切片內：閉半空間、非空軸對齊盒（逐座標區間）與明示有限點集的反例。正面結論都用對所有 p、q、λ 成立的代數證書；不使用拓撲、凸包或分離定理；不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• distributive
• mul_zero
• forall_intro
• quantifier_negation
• cartesian_product_def

• G1 — ℝ² 是實向量空間，加法與純量乘法逐座標進行：(a,b)+(c,d)=(a+c,b+d)，t(a,b)=(ta,tb)。
• G2 — H={(x,y)∈ℝ² ∣ 2x−3y≤6}，法向量 (2,−3)≠(0,0) 的閉半空間。
• G3 — B=[−1,2]×[0,3]={(x,y) ∣ −1≤x≤2 且 0≤y≤3}，非空軸對齊盒。
• G4 — F={(0,0),(2,0),(0,2)}，恰有這三個元素的明示有限點集。

• H — 閉半空間 2x−3y≤6
• B=[-1,2]\times[0,3] — 軸對齊盒
• F — 三點的有限集合
• p=(x_1,y_1),\ q=(x_2,y_2) — 任取的兩點
• \lambda\in[0,1] — 凸組合的權重
• z=\lambda p+(1-\lambda)q — p 與 q 的凸組合

規則與來源

• 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。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• mko_convex · cited — 實向量空間的子集 C 為凸，若對所有 x,y∈C 及所有 λ∈[0,1]，λx+(1−λ)y 仍屬於 C。正例用區間、盒與半空間的完整代數證書；單一精確反例可否證凸性。 · mko-convex-set
• coord_ops · prerequisite — 逐座標運算：(a,b)+(c,d)=(a+c,b+d)，t(a,b)=(ta,tb)。
• ineq_add · prerequisite — 不等式相加：若 u₁≤v₁ 且 u₂≤v₂，則 u₁+u₂≤v₁+v₂。
• L_mono · lemma — 乘以非負數保持不等號：若 u≤v 且 w≥0，則 wu≤wv。
• L_interval · lemma — 區間的凸性證書：若 α≤s≤β、α≤t≤β 且 λ∈[0,1]，則 α≤λs+(1−λ)t≤β。

逐步主鏈

H\ \text{convex}

\forall p,q\in H\ \forall\lambda\in[0,1]:\ \lambda p+(1-\lambda)q\in H

p=(x_1,y_1)\in H,\ q=(x_2,y_2)\in H,\ \lambda\in[0,1]

2x_1-3y_1\le 6,\ 2x_2-3y_2\le 6,\ 0\le\lambda\le 1

z=\lambda p+(1-\lambda)q

z=(\lambda x_1+(1-\lambda)x_2,\ \lambda y_1+(1-\lambda)y_2)

2z_1-3z_2

\lambda(2x_1-3y_1)+(1-\lambda)(2x_2-3y_2)

0\le\lambda\le 1

\lambda\ge 0,\ 1-\lambda\ge 0

2x_1-3y_1\le 6,\ 2x_2-3y_2\le 6

\lambda(2x_1-3y_1)\le 6\lambda,\ (1-\lambda)(2x_2-3y_2)\le 6(1-\lambda)

\lambda(2x_1-3y_1)\le 6\lambda,\ (1-\lambda)(2x_2-3y_2)\le 6(1-\lambda)

2z_1-3z_2\le 6\lambda+6(1-\lambda)=6

2z_1-3z_2\le 6

z\in H\ \text{for all } p,q\in H,\ \lambda\in[0,1];\ H\ \text{convex}

B\ \text{convex}

\forall p,q\in B\ \forall\lambda\in[0,1]:\ -1\le z_1\le 2\ \land\ 0\le z_2\le 3

-1\le x_1,x_2\le 2,\ 0\le y_1,y_2\le 3,\ \lambda\in[0,1]

-1\le z_1\le 2,\ 0\le z_2\le 3

-1\le z_1\le 2,\ 0\le z_2\le 3

z\in B\ \text{for all } p,q\in B,\ \lambda\in[0,1];\ B\ \text{convex}

\neg(F\ \text{convex})

\exists p,q\in F\ \exists\lambda\in[0,1]:\ \lambda p+(1-\lambda)q\notin F

p=(0,0),\ q=(2,0),\ \lambda=\tfrac12

\tfrac12 p+\tfrac12 q=(1,0)

(1,0)\ \text{vs.}\ (0,0),(2,0),(0,2)

(1,0)\notin F

p=(0,0),\ q=(2,0)\in F,\ \lambda=\tfrac12,\ (1,0)\notin F

F\ \text{is not convex}

\lambda\in\{0,1\}

1\cdot p+0\cdot q=p\in F,\ 0\cdot p+1\cdot q=q\in F

局部子步與引理

u\le v,\ w>0

wu\le wv

u\le v,\ w=0

wu=0=wv,\ \text{so}\ wu\le wv

\alpha\le s,\ \alpha\le t

\lambda\alpha+(1-\lambda)\alpha\le\lambda s+(1-\lambda)t

\lambda\alpha+(1-\lambda)\alpha

\alpha

s\le\beta,\ t\le\beta

\lambda s+(1-\lambda)t\le\lambda\beta+(1-\lambda)\beta=\beta

逐步反向審查

• S16 · premise_audit · S15, mul_zero, mul_one — 只用乘以 0 與乘以 1 的性質及 S15。結論是「抽查通過不足以證凸」，由 F 這個具體反例支持；不宣稱任何抽查都會通過。
• S15 · premise_audit · S12, S13, S14, exists_intro — 需要見證中的 p、q 確實屬於 F、λ 確實在 [0,1]，且結果確實不在 F；三者都已核對。
• S14 · premise_audit · G4, cartesian_product_def — 需要 F 的完整列舉（G4 明示只有三點）；若 F 只是「至少含」這三點，此步不成立。
• S13 · inverse_equivalence · coord_ops, numeric_evaluation — 精確的有理數計算，兩邊是同一個點。
• S12 · inverse_equivalence · quantifier_negation, mko_convex — 量詞否定是雙向等價。
• S11 · premise_audit · S09, S10, forall_intro — 需要兩個座標的結論與 p、q、λ 的任意性。
• S10.3 · premise_audit · L_mono, ineq_add, distributive — 與 S10.1 對稱，只用 L_mono、不等式相加與分配律；沒有用 L_interval 本身。
• S10.2 · inverse_equivalence · distributive, mul_one — 反向：α=1·α=(λ+(1−λ))α=λα+(1−λ)α，對所有 λ 成立。
• S10.1 · premise_audit · L_mono, ineq_add, S05 — 本步證明引理 L_interval 的一部分，只用 L_mono 與不等式相加，沒有用 L_interval 本身。
• S10 · premise_audit · S09, L_interval — 需要兩端點都在區間內與 λ∈[0,1]。不宣稱反向：z 在區間內不推出 p、q 都在區間內。
• S09 · inverse_equivalence · cartesian_product_def, mko_convex, G3 — 屬於笛卡兒積等價於每個座標各自屬於對應區間，雙向成立。
• S08 · premise_audit · S07, S02, set_builder, forall_intro — ∀ 引入要求 p、q、λ 任意；S02 至 S07 沒有用到它們的具體值，條件成立。
• S07 · premise_audit · S04, S06, ineq_add, distributive — 需要兩個同向不等式與 S04 的恆等式。相加不可逆：由和的不等式不能推回各自的不等式，所以不宣稱反向。
• S06.2 · premise_audit · S06.1, mul_zero, case_analysis — 兩個情況涵蓋 w≥0 的全部可能；w<0 不在引理範圍內，且那時不等號會反向。
• S06.1 · premise_audit · order_basics, eq_congruence, case_analysis — 需要 w>0；u<v 與 u=v 涵蓋 u≤v 的全部情形。
• S06 · premise_audit · S05, L_mono — 需要兩個權重非負（S05）。不反向宣稱：λ=0 時第一式變成 0≤0，無法還原 2x₁−3y₁≤6。
• S05 · premise_audit · S02, order_basics — 只需 λ∈[0,1]。若 λ 在 [0,1] 之外，其中一個權重為負，S06 不能做；錯誤控制給出這種情形離開 H 的例子。
• S04 · inverse_equivalence · distributive, mul_comm, add_comm — 兩式是同一個多項式，展開與分組可互相還原，對所有實數成立。
• S03 · inverse_equivalence · coord_ops — 兩邊表示同一個有序對，等值代換雙向成立。
• S02 · inverse_equivalence · set_builder, G2 — 對 ℝ² 中的點，屬於 H 與滿足線性不等式是同一件事，雙向成立。
• S01 · inverse_equivalence · mko_convex, def_unfold — 展開定義與收回定義互逆，雙向成立。

錯誤控制與反例

抽查 λ 不能證凸

MKO 指出的誤解是檢查幾個 λ 就宣稱凸。S16 說明 λ=0 與 λ=1 對任何集合都會通過，F 通過了卻不凸。只檢查 λ=1/2 同樣是有限抽樣。H 與 B 的證明對任意 λ∈[0,1] 一次成立，這才是完整證書。

找不到反例不等於凸

若對 F 只嘗試 p=q=(0,0)、λ=1/2，得到 (0,0)∈F，這個見證失敗了，但 F 仍然不凸（S15）。MKO a2：提出的反例失敗，不能反向證明凸性。

權重必須非負

S06 乘不等式時方向不變，只因 λ 與 1−λ 都非負（S05）。若允許 λ=2：p=(3,0)、q=(0,0) 都在 H 中（6≤6、0≤6），但 2p+(1−2)q=(6,0)，2·6−3·0=12>6，離開了 H。所以定義中的 λ∈[0,1] 不能省略。

• 對 F 中所有 p、q，λ=0 與 λ=1 的凸組合都在 F 中，所以 F 是凸的 → reject — 端點抽查對任何集合都通過；λ=1/2 時 (0,0) 與 (2,0) 的中點 (1,0)∉F。
• 嘗試 p=q=(0,0)、λ=1/2 沒有得到 F 外的點，所以 F 是凸的 → reject — 一個見證失敗不證明凸性；另一個見證 (0,0)、(2,0)、λ=1/2 成功否證。
• 對所有實數 λ（不限於 [0,1]），H 都對 λp+(1−λ)q 封閉 → reject — p=(3,0)、q=(0,0)、λ=2 給出 (6,0)，2·6−3·0=12>6。
• B 的凸性必須對每個有理數 λ 分別檢查才算證明 → reject — L_interval 對任意實數 λ∈[0,1] 一次證明，不需要也不能靠逐一檢查（λ 有無限多個）。

結論與限制

閉半空間 H={2x−3y≤6} 與盒 B=[−1,2]×[0,3] 都是凸集合：證明對所有 p、q 與所有 λ∈[0,1] 成立（線性式在凸組合上等於同權重組合，再乘以非負權重相加；盒逐座標用區間證書）。有限點集 F={(0,0),(2,0),(0,2)} 不是凸集合：(0,0) 與 (2,0) 的中點 (1,0) 不在 F 中。

• N6 至 N8、N10、N11 是 S07 的一個具體實例（p=(3,0)、q=(0,−2)、λ=1/3，z=(1,−4/3)），只作示範，證明不依賴它們。
• ineq_add 與 coord_ops 是本稿的前提，不在本稿中由實數公理推出。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 72519a9b66965202b14774efb4fde882285f42c4cd38475be7d32bffffbb565f
• original source SHA-256: 72519a9b66965202b14774efb4fde882285f42c4cd38475be7d32bffffbb565f
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）