面積：半開矩形的交集、聯集與單位格重算

目標與範圍

在等單位正交座標系中，設 A=[0,4)×[0,3)、B=[2,6)×[1,5)。求 A 與 B 的面積，求出交集 A∩B 及其面積，用包含排除求 A∪B 的面積，並以「不同單位格的個數」獨立重算。再設 C=[4,7)×[0,3)（與 A 只在 x=4 處相觸）與 Z=[3,3)×[0,5)（寬為零），求 A∩C、A∪C 的面積與 Z 的面積。

只在 MKO 的受限模型內：整數端點的半開矩形與有限個單位格的聯集。完整證明兩個半開區間的交集公式；矩形面積公式與兩矩形的包含排除取自 MKO 陳述（cited），並以單位格計數對本例獨立重算。不處理一般曲面、可測集、積分或面積的存在性，也不做 Lean 的 box volume 橋接；不改動 canonical MKO 或英文 edition。

已知條件與符號

• numeric_evaluation
• order_basics
• set_operations_def
• cartesian_product_def
• finite_counting_basics

• G1 — 框架與約定：等單位正交座標系；半開約定 [a,b)={x∈ℝ ∣ a≤x<b}；端點為整數；面積單位為所用長度單位的平方（MKO 假設 a1、a3）。
• G2 — A=[0,4)×[0,3)，B=[2,6)×[1,5)。
• G3 — C=[4,7)×[0,3)，Z=[3,3)×[0,5)。

• [a,b) — 半開區間 {x ∣ a≤x<b}
• [x_0,x_1)\times[y_0,y_1) — 半開矩形
• \operatorname{area}(S) — S 的面積（平方單位）
• Q_{i,j} — 單位格 [i,i+1)×[j,j+1)
• \max,\ \min — 兩數中較大、較小者

規則與來源

• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• 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。
• set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
• cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• mko_area_def · cited — 在等單位正交座標系，半開矩形 [x0,x1)×[y0,y1)（x0≤x1、y0≤y1）面積為 (x1−x0)(y1−y0)。任一邊長零時矩形為空、面積零。整數單位格 [i,i+1)×[j,j+1) 面積一，有限聯集面積為不同格子的個數；兩矩形聯集面積為各面積和減交集面積。 · mko-area
• max_min_def · prerequisite — max(u,v)：u≥v 時為 u，否則為 v；min(u,v)：u≤v 時為 u，否則為 v。
• cell_decomp · prerequisite — 對整數 a≤b，[a,b) 是 b−a 個兩兩不交的單位區間 [i,i+1)（i 從 a 到 b−1）的聯集；每個 x∈[a,b) 恰屬於 i=⌊x⌋ 的那一個。
• L_interval_cap · lemma — 對實數 a₀、a₁、b₀、b₁：[a₀,a₁)∩[b₀,b₁)=[max(a₀,b₀), min(a₁,b₁))；當 max(a₀,b₀)≥min(a₁,b₁) 時右邊為空集。

逐步主鏈

\operatorname{area}([x_0,x_1)\times[y_0,y_1))

(x_1-x_0)(y_1-y_0)\quad(x_0\le x_1,\ y_0\le y_1)

\operatorname{area}(A)

(4-0)(3-0)=12

\operatorname{area}(B)

(6-2)(5-1)=16

[0,4)\cap[2,6)

[\max(0,2),\ \min(4,6))=[2,4)

[0,3)\cap[1,5)

[\max(0,1),\ \min(3,5))=[1,3)

A\cap B

([0,4)\cap[2,6))\times([0,3)\cap[1,5))=[2,4)\times[1,3)

\operatorname{area}(A\cap B)

\max(0,4-2)\cdot\max(0,3-1)=2\cdot 2=4

\operatorname{area}(A\cup B)

12+16-4=24

A,\ B

A=\bigcup_{0\le i\le 3,\ 0\le j\le 2}Q_{i,j},\quad B=\bigcup_{2\le i\le 5,\ 1\le j\le 4}Q_{i,j}

A\cup B

\bigcup_{(i,j)\in I_A\cup I_B}Q_{i,j}

|I_A\cup I_B|

4+6+6+4+4=24

A\cap C,\ C=[4,7)\times[0,3)

[\max(0,4),\min(4,7))=[4,4)=\varnothing,\ \operatorname{area}(A\cup C)=12+9-0=21

Z=[3,3)\times[0,5)

Z=\varnothing,\ \operatorname{area}(Z)=(3-3)(5-0)=0,\ \operatorname{area}(A\cup Z)=12

\text{tasks of the goal}

\operatorname{area}(A\cup B)=24,\ \operatorname{area}(A\cup C)=21,\ \operatorname{area}(Z)=0

局部子步與引理

x\in[a_0,a_1)\cap[b_0,b_1)

(a_0\le x\ \land\ b_0\le x)\ \land\ (x<a_1\ \land\ x<b_1)

a_0\le x\ \land\ b_0\le x

\max(a_0,b_0)\le x

x<a_1\ \land\ x<b_1

x<\min(a_1,b_1)

逐步反向審查

• S14 · sufficient_goal_reduction · S02, S03, S07, S08, S11, S12, S13 — 目標 G：題目要求的各個面積。足夠條件 H：S02 到 S13 的結論；H⇒G 只用合取。H 由 G1 到 G3 正向推出，沒有把 G 當作前提。
• S13 · premise_audit · G1, mko_area_def, mul_zero — 空集合與零面積兩件事分別由半開約定與公式得到，互相印證。
• S12 · premise_audit · L_interval_cap, mko_area_def, S02 — 依賴引理與 MKO 的包含排除；只宣稱這一對矩形的結果。
• S11 · inverse_equivalence · finite_counting_basics, numeric_evaluation — 逐列計數是把集合分成互斥部分後的精確計數（N13）；它與 S08 用的是不同方法，兩者一致。
• S10 · inverse_equivalence · set_operations_def, set_extensionality — 聯集定義是雙向的。
• S09 · inverse_equivalence · cell_decomp, cartesian_product_def, set_extensionality — 每點屬於 A 當且僅當它屬於所列某一格，兩集合相等，雙向成立。
• S08 · premise_audit · S02, S03, S07, mko_area_def — 使用的是 MKO 陳述中的公式（cited），本稿未由測度推導；S09 到 S11 以單位格計數對本例獨立重算。
• S07 · inverse_equivalence · mko_area_def, numeric_evaluation — 精確計算（N7 到 N9），雙向成立。
• S06 · inverse_equivalence · cartesian_product_def, set_operations_def, and_intro_elim — 每一個 ⇔ 都是定義展開或合取的重新分組，雙向成立。
• S05 · inverse_equivalence · L_interval_cap, set_extensionality — 與 S04 相同，雙向成立。
• S04.3 · inverse_equivalence · max_min_def, order_basics, case_analysis — 與 S04.2 相同的雙向論證，只是換成上界與嚴格不等式。
• S04.2 · inverse_equivalence · max_min_def, order_basics, case_analysis — 每種情況兩個方向都已說明；兩種情況涵蓋所有 a₀、b₀。
• S04.1 · inverse_equivalence · set_operations_def, and_intro_elim — 交集定義與重新分組都是雙向的。
• S04 · inverse_equivalence · L_interval_cap, set_extensionality — 引理給出兩集合有相同元素（雙向），依集合外延性兩者相等。
• S03 · inverse_equivalence · mko_area_def, numeric_evaluation — 精確整數計算（N2），雙向成立。
• S02 · inverse_equivalence · mko_area_def, numeric_evaluation — 精確整數計算（N1），兩邊是同一個數，雙向成立。
• S01 · premise_audit · G1, mko_area_def — 此步只寫出定義與 MKO 給定的兩個規則，不推出新事實；本稿不由測度論推導這些規則。

錯誤控制與反例

聯集不能直接相加

MKO 指出的誤解是聯集直接相加。12+16=28 把 A∩B 的 4 個單位格算了兩次；扣回一次得 24，與 S11 逐格計數一致。只有在交集面積為零時（如 A 與 C）才可以直接相加。

重複列出的格子不增加面積

Q_{2,1} 同時是 A 與 B 的格子。把 A 的格子與 B 的格子串在一起數會得到 28 筆，但不同格子只有 24 個。面積數的是不同格子（按座標去重），不是列表長度。

零寬矩形沒有面積

Z=[3,3)×[0,5) 的高是 5，但寬是 0，依半開約定它是空集，面積 0（S13）。不能因為某一邊非零就認為它有面積。

• area(A∪B)=12+16=28 → reject — 交集 [2,4)×[1,3) 面積 4 被算兩次；正確值 24。
• Z=[3,3)×[0,5) 的高是 5，所以面積是 5 → reject — 寬 3−3=0，Z 是空集，面積 0·5=0。
• A 與 C 沿 x=4 重疊，所以 area(A∪C)<21 → reject — 4∉[0,4)，A∩C=∅；area(A∪C)=12+9=21。
• A 的面積是 2(4+3)=14 → reject — 14 是周長；面積是 4·3=12（MKO：矩形的幾何量不是周長）。

結論與限制

area(A)=12，area(B)=16，A∩B=[2,4)×[1,3) 面積 4，area(A∪B)=12+16−4=24，並由 24 個不同單位格獨立重算確認。只觸邊的 C 與 A 交集為空，area(A∪C)=21；寬為零的 Z 是空集，面積 0。單位為平方單位。

• 兩矩形的包含排除與「不同單位格聯集的面積等於格數」取自 MKO 陳述，本稿未由測度論推導；S11 的逐格計數只對本例獨立重算。
• cell_decomp（以 ⌊x⌋ 把半開整數區間分成單位區間）作為前提使用，未在本稿證明。
• MKO 的 formal next（二維 box volume 與有限聯集的橋接）未做。

驗證及來源綁定

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

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

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