NRR.EMP.PowerCellPositiveArea — positive area of equal‑area cells

If the weights w are equal‑area for sites s in a body K with 0 < K.area and 0 < n, then every restricted power cell has strictly positive area, and hence (by the theorem interior_nonempty_of_convex_positive_area) nonempty interior.

Public API

• bodyCellArea_pos_of_equalArea — each restricted cell area is strictly positive.
• bodyCellSet_interior_nonempty_of_equalArea — each restricted cell has nonempty interior.

Equal area means each cell carries exactly the average area K.area / n; the coercion n : ℕ ↦ (n : ℝ) is via Nat.cast, so positivity follows from 0 < K.area and 0 < n.

theorem NRR.PowerDiagram.bodyCellArea_pos_of_equalArea {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (hn : 0 < n) (hK : 0 < K.area) (hw : EMP.IsEqualAreaWeight K s w) (i : Fin n) : 0 < bodyCellArea K s w i

Positive area of an equal‑area restricted power cell. With 0 < n and 0 < K.area, if the weights are equal‑area then every restricted cell has strictly positive area, equal to the average K.area / n.

theorem NRR.PowerDiagram.bodyCellSet_interior_nonempty_of_equalArea {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (hn : 0 < n) (hK : 0 < K.area) (hw : EMP.IsEqualAreaWeight K s w) (i : Fin n) : (interior (bodyCellSet K s w i)).Nonempty

Nonempty interior of an equal‑area restricted power cell. With 0 < n and 0 < K.area, if the weights are equal‑area then every restricted cell has nonempty interior. Uses the theorem that a compact convex planar set with positive area has nonempty interior.