IndisputableMonolith.RecogSpec.ClosureShim

   1import IndisputableMonolith.RecogSpec.Spec
   2import IndisputableMonolith.RecogSpec.InevitabilityScaffold
   3
   4namespace IndisputableMonolith
   5namespace RecogSpec
   6
   7/-- Lightweight derivation of `Recognition_Closure` from the inevitability lemmas.
   8
   9    The component predicates (`Inevitability_dimless`, `Inevitability_absolute`,
  10    and `Recognition_Closure`) are defined in `Spec.lean`.
  11-/
  12theorem recognition_closure_any (φ : ℝ) : Recognition_Closure φ := by
  13  have hDim : Inevitability_dimless φ := inevitability_dimless_holds φ
  14  have hAbs : Inevitability_absolute φ := inevitability_absolute_holds φ
  15  exact recognition_closure_from_inevitabilities (φ:=φ) hDim hAbs
  16
  17end RecogSpec
  18end IndisputableMonolith
  19