NRR.EMP.EqualAreaWeightMaxUnion — the maximal-difference clopen argument

For two equal-area power diagrams, let d i = w' i - w i and let M be the nonempty set of indices where d is maximal. Every M-cell for w equals the corresponding cell for w'. Their union inside the convex body is closed because it is a finite union of closed cells. It is also relatively open: after passing from w to w', every maximal cell beats all nonmaximal sites by a strict amount. Connectedness of the convex body therefore forces that union to be the whole body. Positive area and null overlap then force every index to be maximal.

This supplies the global propagation step needed for uniqueness of equal-area weights without introducing a separate adjacency graph for the power diagram.

theorem NRR.EMP.weightDifference_eq_of_equalArea {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) {w w' : Fin n → ℝ} (hw : IsEqualAreaWeight K s w) (hw' : IsEqualAreaWeight K s w') (i j : Fin n) : w' i - w i = w' j - w j

For two equal-area weight vectors, all coordinate differences w' i - w i are equal.