NRR.EMP.OptimalTransportCore — the isolated optimal‑transport core

This module isolates the single external mathematical dependency needed to obtain equal‑area power weights for a planar convex body: the existence of weights that make every restricted power cell carry the average area K.area / n.

The core theorem

theorem EMP.powerDiagram_equalArea_weights_exists_core
 (K : Geometry.ConvexBody Plane) (s : Fin n → Plane)
 (hn : 0 < n) (hs : Function.Injective s) :
 ∃ w : Fin n → ℝ, EMP.IsEqualAreaWeight K s w

This is the classical Aurenhammer–Hoffmann–Aronov (power / Laguerre diagram) existence result, equivalently the semi‑discrete optimal‑transport existence theorem specialized to the plane with fixed distinct sites and uniform (equal‑area) target masses: for a convex body K of positive area and n pairwise‑distinct sites there exist additive weights w whose Laguerre (power) cells restricted to K all have equal area K.area / n.

Standard proof (convex‑optimization route)

The result is the first‑order optimality condition for a concave, coercive‑modulo‑constants energy on the zero‑sum weight hyperplane {w : ∑ i, w i = 0}:

1. The map w ↦ ∑ i, w i · (target_i) minus the total power‑cell "potential" is concave and coercive modulo the additive‑constant direction (adding a constant to all weights does not change the power diagram; cf. NRR.EMP.WeightShift).
2. Hence it attains a maximum on the zero‑sum hyperplane (Weierstrass on a compact sublevel set / coercivity).
3. The gradient of this energy is exactly the vector of cell‑area deviations EMP.areaDeviation K s w, which is continuous (continuous_areaDeviation_weights) and zero‑sum (sum_areaDeviation_eq_zero).
4. At the maximizer the gradient (projected onto the zero‑sum hyperplane) vanishes, i.e. every cell area equals the common target K.area / n. That is EMP.IsEqualAreaWeight K s w.

The formal proof below uses the continuous area-deviation map, the coercivity estimate, and the outward-field zero theorem. It is consumed by NRR.EMP.exists_equalArea_weights in NRR/EMP/EqualAreaWeightsExistence.lean.

Necessary nondegeneracy hypotheses

• hn : 0 < n — with no sites the target K.area / n is not defined meaningfully and the statement is vacuous/false for a positive‑area body.
• hs : Function.Injective s — the restricted power cells only tile K almost disjointly when the sites are pairwise distinct; coincident sites break the area bookkeeping. This is the same distinct‑site hypothesis carried by sum_EMP_areaVec_eq_area and continuous_EMP_areaVec_weights.

theorem NRR.EMP.powerDiagram_equalArea_weights_exists_core {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) : ∃ (w : Fin n → ℝ), IsEqualAreaWeight K s w

Core semi-discrete optimal transport theorem: for an injective finite site configuration in a positive-area planar convex body, there are power weights whose restricted power cells have equal area. This theorem is the core existence result used by the equal-area weight API.