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

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

\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

Substeps and lemmas

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)

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 add

The 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 area

Q_{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 area

Z=[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)