Internal Model

@[reducible, inline]

abbrev NRR.HumanExport.Plane : Type

The Euclidean plane used by the internal proof-export layer.

Equations

• NRR.HumanExport.Plane = EuclideanSpace ℝ (Fin 2)

class NRR.HumanExport.ConvexFigureModel (α : Type) : Type

A type-level interface used by the proof wrapper.

The human-facing structure is deliberately declared later, in HumanVerification/Main.lean. This interface lets the wrapper be imported before that declaration, avoiding an import cycle while keeping all public definitions in the human-facing file.

• carrier : α → Set Plane

  The set of planar points represented by a figure.

• isConvex (F : α) : Convex ℝ (carrier F)
• isCompact (F : α) : IsCompact (carrier F)
• hasNonemptyInterior (F : α) : (interior (carrier F)).Nonempty
• ofBody : Geometry.ConvexBody Plane → α

  Represent a convex body in the chosen external figure model.

• carrier_ofBody (K : Geometry.ConvexBody Plane) : carrier (ofBody K) = K.carrier

def NRR.HumanExport.ConvexFigureModel.toBody {α : Type} [ConvexFigureModel α] (F : α) : Geometry.ConvexBody Plane

Convert any model value into the convex-body type used by NRR.

Equations

• NRR.HumanExport.ConvexFigureModel.toBody F = { carrier := NRR.HumanExport.ConvexFigureModel.carrier F, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := ⋯ }

@[simp]

theorem NRR.HumanExport.ConvexFigureModel.toBody_carrier {α : Type} [ConvexFigureModel α] (F : α) : (toBody F).carrier = carrier F

@[simp]

theorem NRR.HumanExport.ConvexFigureModel.carrier_ofBody_apply {α : Type} [ConvexFigureModel α] (K : Geometry.ConvexBody Plane) : carrier (ofBody K) = K.carrier

@[reducible, inline]

noncomputable abbrev NRR.HumanExport.area {α : Type} [ConvexFigureModel α] (F : α) : ENNReal

Generic area used internally by the wrapper.

Equations

• NRR.HumanExport.area F = MeasureTheory.volume (NRR.HumanExport.ConvexFigureModel.carrier F)

@[reducible, inline]

noncomputable abbrev NRR.HumanExport.perimeter {α : Type} [ConvexFigureModel α] (F : α) : ENNReal

Generic Hausdorff perimeter used internally by the wrapper.

Equations

• NRR.HumanExport.perimeter F = (MeasureTheory.Measure.hausdorffMeasure 1) (frontier (NRR.HumanExport.ConvexFigureModel.carrier F))

@[reducible, inline]

abbrev NRR.HumanExport.IsConvexPartition {α : Type} [ConvexFigureModel α] {n : ℕ} (F : α) (pieces : Fin n → α) : Prop

Generic partition predicate used internally by the wrapper.

Equations

• One or more equations did not get rendered due to their size.