NRR.Partition.ConvexPartition — the shared convex‑partition structure

This module defines the single, shared ConvexPartition structure used by all later fair‑partition modules, together with the basic cover/subset/area API needed before area additivity can be developed.

The structure is stated over the unified public body type NRR.Body, which is a definitional alias of NRR.Geometry.ConvexBody NRR.E2 = ConvexBody Plane (E2 = Geometry.Plane). No independent convex‑body API is introduced here.

Hypotheses

The partition records exactly the data needed for finite measure additivity of the area functional:

• subset — each piece is contained in K;
• covers — the pieces cover K;
• nullOverlap — distinct pieces overlap only on a Lebesgue‑null set.

Strict (set‑theoretic) disjointness is deliberately not required: null overlaps are exactly what finite measure additivity needs and what power/Voronoi partitions actually satisfy.

API

• ConvexPartition.IsEqualArea — all pieces have equal area.
• ConvexPartition.iUnion_piece_eq — the pieces union to K (as sets).
• ConvexPartition.piece_subset — each piece is a subset of K.
• ConvexPartition.piece_area_nonneg — each piece has nonnegative area.

Area additivity itself is intentionally not proved here.

structure NRR.ConvexPartition (K : Body) (n : ℕ) : Type

A convex partition of a body K into n convex pieces (convex bodies) that cover K and overlap only on null sets.

The body type Body is the unified public alias of ConvexBody Plane (Body = Geometry.ConvexBody E2, E2 = Geometry.Plane).

• piece : Fin n → Body

  The i‑th convex piece.

• subset (i : Fin n) : (self.piece i).carrier ⊆ K.carrier

  Each piece is contained in K.

• covers : K.carrier ⊆ ⋃ (i : Fin n), (self.piece i).carrier

  The pieces cover K.

• nullOverlap (i j : Fin n) : i ≠ j → MeasureTheory.volume ((self.piece i).carrier ∩ (self.piece j).carrier) = 0

  Distinct pieces overlap only on a null set.

def NRR.ConvexPartition.IsEqualArea {K : Body} {n : ℕ} (P : ConvexPartition K n) : Prop

All pieces have equal area.

Equations

• P.IsEqualArea = ∀ (i j : Fin n), NRR.Geometry.ConvexBody.area (P.piece i) = NRR.Geometry.ConvexBody.area (P.piece j)

theorem NRR.ConvexPartition.iUnion_piece_eq {K : Body} {n : ℕ} (P : ConvexPartition K n) : ⋃ (i : Fin n), (P.piece i).carrier = K.carrier

The pieces of a convex partition union (as sets) to the whole body K.

theorem NRR.ConvexPartition.piece_subset {K : Body} {n : ℕ} (P : ConvexPartition K n) (i : Fin n) : (P.piece i).carrier ⊆ K.carrier

Each piece of a convex partition is a subset of the ambient body K.

theorem NRR.ConvexPartition.piece_area_nonneg {K : Body} {n : ℕ} (P : ConvexPartition K n) (i : Fin n) : 0 ≤ Geometry.ConvexBody.area (P.piece i)

Each piece of a convex partition has nonnegative area.