`IndisputableMonolith.Verification.MetricCurvatureCert`

IndisputableMonolith/Verification/MetricCurvatureCert.lean · 20 lines · 1 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Verification.CurvatureSpaceCert
   3
   4namespace IndisputableMonolith.Verification.MetricCurvature
   5
   6structure MetricCurvatureCert where
   7  deriving Repr
   8
   9/-- Verification of Metric & Curvature Grounding. -/
  10@[simp] def MetricCurvatureCert.verified (_c : MetricCurvatureCert) : Prop :=
  11  IndisputableMonolith.Verification.CurvatureSpace.CurvatureSpaceCert.verified {}
  12
  13@[simp] theorem MetricCurvatureCert.verified_any (c : MetricCurvatureCert) :
  14    MetricCurvatureCert.verified c := by
  15  simpa [MetricCurvatureCert.verified] using
  16    (IndisputableMonolith.Verification.CurvatureSpace.CurvatureSpaceCert.verified_any {})
  17
  18end MetricCurvature
  19end IndisputableMonolith.Verification
  20

source mirrored from github.com/jonwashburn/shape-of-logic