NRR.EMP.NormalizedWeightSelection — canonical normalized equal‑area weight

This module proves that normalized equal‑area weights are unique (as a Subsingleton of the subtype EMP.NormalizedEqualAreaWeight), and then selects a canonical representative, EMP.normalizedWeight, via Classical.choice of the existence result from the existing existence theorem.

Results

• EMP.normalized_equalArea_weight_subsingleton — the subtype of normalized equal‑area weights is a subsingleton (uniqueness), from the normalized uniqueness theorem EMP.equalArea_weights_unique_normalized.
• EMP.normalizedWeight — the selected canonical normalized equal‑area weight vector, Classical.choice of EMP.exists_normalized_equalArea_weight (the existing existence theorem).
• EMP.normalizedWeight_isEqualArea — the selected weight is equal‑area.
• EMP.normalizedWeight_normalized — the selected weight is normalized.
• EMP.normalizedWeight_unique — any equal‑area normalized weight equals the selected one.

theorem NRR.EMP.normalized_equalArea_weight_subsingleton {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) : Subsingleton (NormalizedEqualAreaWeight K s)

Uniqueness of normalized equal‑area weights. The subtype of weight vectors that are simultaneously equal‑area and normalized is a subsingleton: any two of its elements are equal. This packages the normalized uniqueness theorem EMP.equalArea_weights_unique_normalized. The hypothesis hn : 0 < n is retained to match the required public API signature, even though this particular proof does not use it.

noncomputable def NRR.EMP.normalizedWeight {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) : Fin n → ℝ

Selected normalized equal‑area weight. A canonical choice of a weight vector that is both equal‑area for the sites s in K and normalized (∑ i, w i = 0), obtained by Classical.choice from the existence theorem EMP.exists_normalized_equalArea_weight (the existing existence theorem). By EMP.normalized_equalArea_weight_subsingleton this choice is in fact unique.

Equations

• NRR.EMP.normalizedWeight K s hn hs = ↑(Classical.choice ⋯)

theorem NRR.EMP.normalizedWeight_isEqualArea {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) : IsEqualAreaWeight K s (normalizedWeight K s hn hs)

The selected normalized weight is an equal‑area weight.

theorem NRR.EMP.normalizedWeight_normalized {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) : WeightNormalized (normalizedWeight K s hn hs)

The selected normalized weight is normalized (∑ i, w i = 0).

theorem NRR.EMP.normalizedWeight_unique {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) {w : Fin n → ℝ} (hw : IsEqualAreaWeight K s w) (hnorm : WeightNormalized w) : w = normalizedWeight K s hn hs

Canonicity. Any equal‑area normalized weight equals the selected normalized weight, by the subsingleton property of normalized equal‑area weights.