NRR.PowerDiagram.CellOverlap — null overlap of distinct power cells

Two distinct nondegenerate power (Laguerre) cells overlap only on the radical hyperplane (bisector) of the two sites, and this overlap is Lebesgue‑null; consequently their interiors are disjoint.

The nondegeneracy hypothesis is sepNormal s i j ≠ 0, i.e. s i ≠ s j (the two sites are distinct). Without it the theorem is false: if s i = s j and w i = w j then the two cells coincide and their overlap has positive volume.

• cell_inter_subset_bisector — the overlap of two cells is contained in the bisector hyperplane {x | ⟪sepNormal s i j, x⟫ = sepOffset s w i j}.
• cell_inter_null — the overlap of two distinct nondegenerate cells is Lebesgue‑null.
• interior_cell_disjoint — distinct nondegenerate cells have disjoint interiors.

The ambient type is the library alias E2 = Geometry.Plane = EuclideanSpace ℝ (Fin 2) (this is the Plane referred to in the design).

theorem NRR.PowerDiagram.cell_inter_subset_bisector {n : ℕ} (s : Fin n → E2) (w : Fin n → ℝ) {i j : Fin n} : cell s w i ∩ cell s w j ⊆ {x : E2 | inner ℝ (sepNormal s i j) x = sepOffset s w i j}

The overlap of the power cells of i and j is contained in the radical (bisector) hyperplane {x | ⟪sepNormal s i j, x⟫ = sepOffset s w i j}: on the overlap the two power distances are equal (each ≤ the other), which is exactly membership in the hyperplane.

theorem NRR.PowerDiagram.cell_inter_null {n : ℕ} (s : Fin n → E2) (w : Fin n → ℝ) {i j : Fin n} (hij : sepNormal s i j ≠ 0) : MeasureTheory.volume (cell s w i ∩ cell s w j) = 0

Pairwise overlaps of distinct nondegenerate cells are Lebesgue‑null: the overlap lies in a hyperplane with nonzero normal, which is null.

theorem NRR.PowerDiagram.interior_cell_disjoint {n : ℕ} (s : Fin n → E2) (w : Fin n → ℝ) {i j : Fin n} (hij : sepNormal s i j ≠ 0) : Disjoint (interior (cell s w i)) (interior (cell s w j))

Distinct nondegenerate power cells have disjoint interiors: their intersection is an open set contained in a null hyperplane, hence empty.