NRR.EMP.EqualAreaWeightCellRigidity — maximal weight differences fix a cell

Let w and w' be two weight vectors and put d i = w' i - w i. If d i is maximal, then the i-th power cell for w is contained in the i-th power cell for w'. If both weight vectors give the same positive prescribed cell area, compact-convex area rigidity upgrades this inclusion to equality.

This is the elementary geometric core of uniqueness up to an additive constant. The remaining global uniqueness step is to propagate equality of the maximal difference across the cell adjacency graph.

theorem NRR.PowerDiagram.bodyCellSet_subset_of_weightDifference_max {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w w' : Fin n → ℝ) (i : Fin n) (hmax : ∀ (j : Fin n), w' j - w j ≤ w' i - w i) : bodyCellSet K s w i ⊆ bodyCellSet K s w' i

If w' i - w i is maximal among all coordinate differences, the i-th restricted power cell for w is contained in the corresponding cell for w'.

theorem NRR.PowerDiagram.bodyCellSet_eq_of_equalArea_of_weightDifference_max {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) {w w' : Fin n → ℝ} (hw : EMP.IsEqualAreaWeight K s w) (hw' : EMP.IsEqualAreaWeight K s w') (i : Fin n) (hmax : ∀ (j : Fin n), w' j - w j ≤ w' i - w i) : bodyCellSet K s w i = bodyCellSet K s w' i

For two equal-area weight vectors, a coordinate at which w' - w is maximal has exactly the same restricted power cell for both vectors.