NRR.BodySpace.AreaRigidity — area rigidity for nested convex subbodies

This module proves the geometric rigidity statement used to identify a Hausdorff limit of canonical cells: if one compact convex planar set is strictly contained in another with nonempty interior, its Lebesgue area is strictly smaller. The consequence for the fixed-parent hyperspace is that a nested pair of convex subbodies with equal positive area must coincide.

The set-level argument is elementary: a point of interior D lies outside the closed set C (else D = closure (interior D) ⊆ C, contradicting strictness), and a small ball around that point sits inside D and misses C, contributing strictly positive extra area.

theorem NRR.measure_lt_of_compact_convex_ssubset {C D : Set Geometry.Plane} (hCcomp : IsCompact C) (hDcomp : IsCompact D) (hDconv : Convex ℝ D) (hCD : C ⊂ D) (hDint : (interior D).Nonempty) : (MeasureTheory.volume C).toReal < (MeasureTheory.volume D).toReal

Strict area monotonicity for nested compact convex bodies. If C ⊂ D with C, D compact and convex and D of nonempty interior, then C has strictly smaller Lebesgue area than D.

The convexity of C (hCconv) is part of the intended interface but is not needed for the proof: only the compactness (hence closedness) of C and the convexity and nonempty interior of D enter the argument.

theorem NRR.ConvexSubbody.eq_of_subset_of_area_eq {K : Geometry.ConvexBody Geometry.Plane} {C D : ConvexSubbody K} (hCD : ↑C.body ⊆ ↑D.body) (harea : C.area = D.area) (hDpos : 0 < D.area) : C = D

Area rigidity for nested convex subbodies. If the carrier of C is contained in that of D, both have equal area, and D has positive area, then C = D.

theorem NRR.ConvexSubbody.eq_of_subset_of_area_eq' {K : Geometry.ConvexBody Geometry.Plane} {C D : ConvexSubbody K} (hCD : ↑C.body ⊆ ↑D.body) (harea : C.area = D.area) (hDpos : 0 < D.area) : C = D

Ergonomic form of eq_of_subset_of_area_eq phrased with the subbody-to-set coercion.