# Area: intersection and union of half-open rectangles, recounted by unit cells

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-area/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-area-01 · production-20261019-adopted-96



## Goal and scope

In an equal-unit orthonormal frame let A=[0,4)×[0,3) and B=[2,6)×[1,5). Find the areas of A and B, find the intersection A∩B and its area, find the area of A∪B by inclusion and exclusion, and recount it independently as the number of distinct unit cells. Then let C=[4,7)×[0,3) (touching A only at x=4) and Z=[3,3)×[0,5) (zero width), and find the areas of A∩C, A∪C and Z.

Stays inside the MKO's restricted model: half-open rectangles with integer endpoints and finite unions of unit cells. It fully proves the intersection formula for two half-open intervals; the rectangle area formula and inclusion and exclusion for two rectangles are taken from the MKO statement (cited) and are recounted independently for this example by counting unit cells. It does not treat general surfaces, measurable sets, integrals or the existence of area, and does not build the Lean box-volume bridge; it does not change the canonical MKO or its English edition.





## Givens and symbols


- numeric_evaluation
- order_basics
- set_operations_def
- cartesian_product_def
- finite_counting_basics


- G1 — Frame and conventions: an equal-unit orthonormal frame; the half-open convention [a,b)={x∈ℝ ∣ a≤x<b}; integer endpoints; area is measured in the square of the chosen length unit (MKO assumptions a1, a3).
- G2 — A=[0,4)×[0,3) and B=[2,6)×[1,5).
- G3 — C=[4,7)×[0,3) and Z=[3,3)×[0,5).


- [a,b) — the half-open interval {x ∣ a≤x<b}
- [x_0,x_1)\times[y_0,y_1) — a half-open rectangle
- \operatorname{area}(S) — the area of S (square units)
- Q_{i,j} — the unit cell [i,i+1)×[j,j+1)
- \max,\ \min — the larger and the smaller of two numbers





## Rules and sources


- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
- cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
- finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- mko_area_def · cited — In an equal-unit orthonormal frame, a half-open rectangle [x0,x1)×[y0,y1) with x0≤x1 and y0≤y1 has area (x1−x0)(y1−y0). Zero width or height makes it empty, with area zero. An integer unit cell [i,i+1)×[j,j+1) has area one, and a finite union of distinct such cells has area equal to their count. For two such rectangles, area(A∪B)=area(A)+area(B)−area(A∩B). · mko-area
- max_min_def · prerequisite — max(u,v) is u if u≥v and v otherwise; min(u,v) is u if u≤v and v otherwise.
- cell_decomp · prerequisite — For integers a≤b, [a,b) is the union of the b−a pairwise disjoint unit intervals [i,i+1) with i running from a to b−1; each x∈[a,b) lies in exactly the one with i=⌊x⌋.
- L_interval_cap · lemma — For reals a₀, a₁, b₀, b₁: [a₀,a₁)∩[b₀,b₁)=[max(a₀,b₀), min(a₁,b₁)); when max(a₀,b₀)≥min(a₁,b₁) the right side is empty.





## Main derivation

S01 · definitionBefore

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

After

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

Conditions: x_0\le x_1; y_0\le y_1

Rule: mko_area_def · Uses: G1

Leaf basis: mko_area_def + def_unfold

State the MKO's restricted model: a half-open rectangle with ordered endpoints has area width times height; a unit cell has area one, and a finite union of distinct unit cells has area equal to their number; the area of the union of two rectangles is the sum of their areas minus the area of their intersection. Area is measured in square units and is not the perimeter.



S02 · equivalentBefore

\operatorname{area}(A)

After

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

Conditions: 0\le 4; 0\le 3

Rule: mko_area_def · Uses: S01, G2

Leaf basis: mko_area_def + numeric_evaluation

A=[0,4)×[0,3) has ordered endpoints (0≤4, 0≤3), so the formula of S01 applies: width 4−0=4, height 3−0=3, area 4·3=12 square units.



S03 · equivalentBefore

\operatorname{area}(B)

After

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

Conditions: 2\le 6; 1\le 5

Rule: mko_area_def · Uses: S01, G2

Leaf basis: mko_area_def + numeric_evaluation

B=[2,6)×[1,5): width 6−2=4, height 5−1=4, area 16 square units. The width is the right endpoint minus the left endpoint, not the right endpoint itself.



S04 · equivalentBefore

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

After

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

Conditions: none

Rule: L_interval_cap · Uses: G2, L_interval_cap

Leaf basis: L_interval_cap + numeric_evaluation

By Lemma L_interval_cap (a₀=0, a₁=4, b₀=2, b₁=6) the intersection of the two x-intervals is [max(0,2), min(4,6))=[2,4). The lemma is proved in S04.1 to S04.3.



S05 · equivalentBefore

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

After

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

Conditions: none

Rule: L_interval_cap · Uses: G2, L_interval_cap

Leaf basis: L_interval_cap + numeric_evaluation

Apply the same lemma to the y-intervals (a₀=0, a₁=3, b₀=1, b₁=5): the intersection is [1,3).



S06 · equivalentBefore

A\cap B

After

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

Conditions: none

Rule: cartesian_product_def · Uses: S04, S05, G2

Leaf basis: cartesian_product_def + set_operations_def + and_intro_elim

(x,y)∈A∩B ⇔ (x∈[0,4) and y∈[0,3)) and (x∈[2,6) and y∈[1,5)) ⇔ x∈[0,4)∩[2,6) and y∈[0,3)∩[1,5). So the intersection of two rectangles is again a rectangle whose sides are the intersections of the corresponding intervals; substituting S04 and S05 gives [2,4)×[1,3).



S07 · equivalentBefore

\operatorname{area}(A\cap B)

After

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

Conditions: 2\le 4; 1\le 3

Rule: mko_area_def · Uses: S01, S06

Leaf basis: mko_area_def + max_min_def + numeric_evaluation

By MKO assumption a2 the width of the intersection is max(0, min(upper endpoints)−max(lower endpoints))=max(0,4−2)=2 and the height is max(0,3−1)=2. The outer max(0, ·) makes the width 0 rather than negative when the intersection is empty. Here 2≤4 and 1≤3, so [2,4)×[1,3) is a rectangle with ordered endpoints and area 4.



S08 · theorem_applicationBefore

\operatorname{area}(A\cup B)

After

12+16-4=24

Conditions: none

Rule: mko_area_def · Uses: S02, S03, S07, mko_area_def

Leaf basis: mko_area_def + numeric_evaluation

By the MKO's inclusion and exclusion for two rectangles: area(A∪B)=area(A)+area(B)−area(A∩B)=12+16−4=24. The intersection is counted in both A and B, so it is subtracted once; adding directly to get 28 would count it twice.



S09 · equivalentBefore

A,\ B

After

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}

Conditions: none

Rule: cell_decomp · Uses: G1, G2, cell_decomp

Leaf basis: cell_decomp + cartesian_product_def + finite_counting_basics

By cell_decomp, [0,4) is the union of [i,i+1) for i=0,1,2,3 and [0,3) is the union of [j,j+1) for j=0,1,2; the Cartesian product of two unions is the union of the products of the pairs, so A is the union of 4·3=12 unit cells Q_{i,j}. Likewise B is the union of the 16 cells with i∈{2,3,4,5} and j∈{1,2,3,4}. The half-open convention makes distinct cells pairwise disjoint: each point lies only in the cell (⌊x⌋,⌊y⌋).



S10 · equivalentBefore

A\cup B

After

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

Conditions: none

Rule: set_operations_def · Uses: S09, set_operations_def

Leaf basis: set_operations_def + set_extensionality

Let I_A and I_B be the index sets of the cells of A and B. A point is in A∪B ⇔ it is in a cell with (i,j)∈I_A or in one with (i,j)∈I_B ⇔ it is in a cell with (i,j)∈I_A∪I_B. Indices are merged as a set, so a cell appearing on both sides (for example Q_{2,1}) counts once (MKO assumption a3: deduplicate by coordinates).



S11 · equivalentBefore

|I_A\cup I_B|

After

4+6+6+4+4=24

Conditions: none

Rule: finite_counting_basics · Uses: S10, S09, finite_counting_basics, mko_area_def

Leaf basis: finite_counting_basics + mko_area_def + numeric_evaluation

Count the distinct i row by row (fixed j): for j=0 only A contributes, i∈{0,1,2,3}, 4 cells; for j=1, A gives {0,1,2,3} and B gives {2,3,4,5}, merging to {0,1,2,3,4,5}, 6 cells; j=2 likewise 6 cells; j=3 only B, {2,3,4,5}, 4 cells; j=4 also 4 cells. Different rows are disjoint, so the counts add (finite_counting_basics) to 24. By the MKO the area of a union of distinct unit cells is their number, so area(A∪B)=24, in agreement with S08.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: L_interval_cap · Uses: G3, L_interval_cap, S01, S02

Leaf basis: L_interval_cap + mko_area_def + numeric_evaluation

In the x-direction: [0,4)∩[4,7)=[max(0,4), min(4,7))=[4,4), and no x satisfies 4≤x<4, so it is empty; hence A∩C=∅, width max(0,4−4)=0 and intersection area 0. The area of C is (7−4)(3−0)=9, so area(A∪C)=12+9−0=21. For example (4,1)∈C but 4∉[0,4), so (4,1)∉A: two half-open rectangles that merely touch share no point.



S13 · impliesBefore

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

After

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

Conditions: 3\le 3

Rule: mko_area_def · Uses: G1, G3, S01, S02

Leaf basis: mko_area_def + mul_zero + set_operations_def

By the half-open convention, [3,3) needs 3≤x<3, which no x satisfies, so [3,3)=∅ and Z=∅×[0,5)=∅. The formula also gives (3−3)(5−0)=0·5=0 (mul_zero). A∪Z=A∪∅=A, whose area is still 12. A height of 5 does not give the empty rectangle any area (MKO: zero width or height makes the rectangle empty, with area zero).



S14 · impliesBefore

\text{tasks of the goal}

After

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

Conditions: none

Rule: and_intro_elim · Uses: S02, S03, S07, S08, S11, S12, S13

Leaf basis: and_intro_elim

Combine: area(A)=12, area(B)=16, A∩B=[2,4)×[1,3) with area 4, area(A∪B)=24 (inclusion and exclusion and the cell count agree), A∩C=∅ and area(A∪C)=21, area(Z)=0. Every area value is in square units.







## Substeps and lemmas

S04.1 · equivalentBefore

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

After

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

Conditions: none

Rule: set_operations_def · Uses: set_operations_def, G1

Leaf basis: set_operations_def + and_intro_elim

By the definition of intersection, x lies in the intersection ⇔ x∈[a₀,a₁) and x∈[b₀,b₁). By the half-open convention (G1) each membership is a pair of inequalities. Regroup the four conjuncts, putting the two lower-bound conditions together and the two upper-bound conditions together; conjunction is commutative and associative, so the truth value is unchanged.



S04.2 · equivalentBefore

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

After

\max(a_0,b_0)\le x

Conditions: none

Rule: case_analysis · Uses: S04.1, max_min_def

Leaf basis: case_analysis + max_min_def + order_basics

Split into two cases (covering everything by trichotomy). Case a₀≥b₀: max(a₀,b₀)=a₀. Forward: a₀≤x gives it directly. Backward: a₀≤x, and b₀≤a₀≤x gives b₀≤x by transitivity. Case a₀<b₀: max(a₀,b₀)=b₀ and the roles exchange, with the same argument.



S04.3 · equivalentBefore

x<a_1\ \land\ x<b_1

After

x<\min(a_1,b_1)

Conditions: none

Rule: case_analysis · Uses: S04.1, S04.2, max_min_def

Leaf basis: case_analysis + max_min_def + order_basics

Case a₁≤b₁: min(a₁,b₁)=a₁. Forward is immediate; backward: x<a₁≤b₁ gives x<b₁. Case a₁>b₁: min=b₁, the same. Combining with S04.1 and S04.2: x∈[a₀,a₁)∩[b₀,b₁) ⇔ max(a₀,b₀)≤x<min(a₁,b₁) ⇔ x∈[max(a₀,b₀), min(a₁,b₁)). If max(a₀,b₀)≥min(a₁,b₁), no x satisfies both inequalities and the intersection is empty. S04.1 to S04.3 together prove Lemma L_interval_cap.







## Reverse audits


- S14 · sufficient_goal_reduction · S02, S03, S07, S08, S11, S12, S13 — Goal G: the areas asked for. Sufficient condition H: the conclusions of S02 to S13; H⇒G uses only conjunction. H is derived forwards from G1 to G3; G is never used as a premise.
- S13 · premise_audit · G1, mko_area_def, mul_zero — Emptiness and zero area come separately from the half-open convention and from the formula, and they confirm each other.
- S12 · premise_audit · L_interval_cap, mko_area_def, S02 — It relies on the lemma and the MKO's inclusion and exclusion; it claims the result for this pair only.
- S11 · inverse_equivalence · finite_counting_basics, numeric_evaluation — The row count is an exact count after splitting the set into disjoint parts (N13); it uses a different method from S08, and the two agree.
- S10 · inverse_equivalence · set_operations_def, set_extensionality — The definition of union is two-way.
- S09 · inverse_equivalence · cell_decomp, cartesian_product_def, set_extensionality — A point is in A exactly when it is in one of the listed cells, so the sets are equal, two-way.
- S08 · premise_audit · S02, S03, S07, mko_area_def — The formula used is the one in the MKO statement (cited) and is not derived here from a measure; S09 to S11 recount this example independently by unit cells.
- S07 · inverse_equivalence · mko_area_def, numeric_evaluation — Exact computation (N7 to N9), two-way.
- S06 · inverse_equivalence · cartesian_product_def, set_operations_def, and_intro_elim — Each ⇔ is an unfolding of a definition or a regrouping of conjunctions, so it is two-way.
- S05 · inverse_equivalence · L_interval_cap, set_extensionality — As in S04, two-way.
- S04.3 · inverse_equivalence · max_min_def, order_basics, case_analysis — The same two-way argument as in S04.2, with upper bounds and strict inequalities.
- S04.2 · inverse_equivalence · max_min_def, order_basics, case_analysis — Both directions are argued in each case, and the two cases cover all a₀, b₀.
- S04.1 · inverse_equivalence · set_operations_def, and_intro_elim — The definition of intersection and the regrouping are both two-way.
- S04 · inverse_equivalence · L_interval_cap, set_extensionality — The lemma shows that the two sets have the same elements (both directions), so they are equal by extensionality.
- S03 · inverse_equivalence · mko_area_def, numeric_evaluation — An exact integer computation (N2), two-way.
- S02 · inverse_equivalence · mko_area_def, numeric_evaluation — An exact integer computation (N1); both sides are the same number, so it holds both ways.
- S01 · premise_audit · G1, mko_area_def — This step only states the definition and the two rules given by the MKO; it derives no new fact. This guide does not derive these rules from measure theory.





## Error controls and negative controls

Areas of a union do not simply addThe misconception the MKO names is adding areas of a union directly. 12+16=28 counts the 4 unit cells of A∩B twice; subtracting them once gives 24, which matches the cell count in S11. Areas may be added directly only when the intersection has area zero (as for A and C).

A cell listed twice adds no areaQ_{2,1} is a cell of both A and B. Concatenating the cell lists of A and B gives 28 entries, but there are only 24 distinct cells. Area counts distinct cells (deduplicated by coordinates), not the length of a list.

A zero-width rectangle has no areaZ=[3,3)×[0,5) has height 5 but width 0; by the half-open convention it is empty and has area 0 (S13). A nonzero side does not give it area.


- area(A∪B)=12+16=28 → reject — The intersection [2,4)×[1,3) of area 4 is counted twice; the correct value is 24.
- Z=[3,3)×[0,5) has height 5, so its area is 5 → reject — The width is 3−3=0, Z is empty, and its area is 0·5=0.
- A and C overlap along x=4, so area(A∪C)<21 → reject — 4∉[0,4), so A∩C=∅ and area(A∪C)=12+9=21.
- The area of A is 2(4+3)=14 → reject — 14 is the perimeter; the area is 4·3=12 (MKO: the area of a rectangle is not its perimeter).





## Result and limitations

area(A)=12, area(B)=16, A∩B=[2,4)×[1,3) with area 4, and area(A∪B)=12+16−4=24, confirmed independently by 24 distinct unit cells. C merely touches A, so A∩C=∅ and area(A∪C)=21; Z has zero width, is empty and has area 0. Units are square units.


- Inclusion and exclusion for two rectangles and 'the area of a union of distinct unit cells is their number' are taken from the MKO statement and are not derived from measure theory here; the cell count in S11 recounts this example only.
- cell_decomp (splitting a half-open integer interval into unit intervals by ⌊x⌋) is used as a prerequisite and is not proved here.
- The MKO's formal next step (bridging two-dimensional box volume and finite unions) is not done.





## Verification and source binding

19 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-area-01.json)