NRR.FairPartition.Predicates — the public fair-partition predicate

This module fixes the single, public fair partition predicate used by the final Nandakumar–Ramana Rao assembly. A convex partition is fair when

• all pieces have equal area (ConvexPartition.IsEqualArea), and
• all pieces have equal perimeter (ConvexPartition.HasEqualPerimeter).

Both underlying predicates already exist and are reused unchanged:

• ConvexPartition.IsEqualArea — from NRR.Partition.ConvexPartition;
• ConvexPartition.HasEqualPerimeter — from NRR.Partition.PerimeterVector.

No new partition structure is introduced and ConvexPartition is not redefined.

API

• ConvexPartition.IsFair — the fair-partition predicate (a conjunction of the two above).
• ConvexPartition.IsFair.equalArea — projection to the equal-area component.
• ConvexPartition.IsFair.equalPerimeter — projection to the equal-perimeter component.
• ConvexPartition.isFair_iff — unfolding lemma exposing the conjunction.
• ConvexPartition.IsFair.mk' — build IsFair from the two components.

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

A fair partition: all pieces have equal area and all pieces have equal perimeter.

Equations

• P.IsFair = (P.IsEqualArea ∧ P.HasEqualPerimeter)

theorem NRR.ConvexPartition.isFair_iff {K : Body} {n : ℕ} {P : ConvexPartition K n} : P.IsFair ↔ P.IsEqualArea ∧ P.HasEqualPerimeter

Unfolding lemma: IsFair is exactly the conjunction of equal area and equal perimeter.

theorem NRR.ConvexPartition.IsFair.equalArea {K : Body} {n : ℕ} {P : ConvexPartition K n} (h : P.IsFair) : P.IsEqualArea

A fair partition has all pieces of equal area.

theorem NRR.ConvexPartition.IsFair.equalPerimeter {K : Body} {n : ℕ} {P : ConvexPartition K n} (h : P.IsFair) : P.HasEqualPerimeter

A fair partition has all pieces of equal perimeter.

theorem NRR.ConvexPartition.IsFair.mk' {K : Body} {n : ℕ} {P : ConvexPartition K n} (hA : P.IsEqualArea) (hP : P.HasEqualPerimeter) : P.IsFair

Build a fair partition from equal area and equal perimeter.