  88
  89/-- Route B certificate: specifiability is exactly the same floor as a
  90non-singleton universe of discourse. -/
  91structure SpecifiabilityClosureCert (K : Type*) [Nonempty K] : Prop where
  92  equivalence :
  93    (∃ x y : K, x ≠ y) ↔ Nonempty (NontrivialSpecification K)
  94
  95/-- The specifiability closure certificate is theorem-backed. -/
  96theorem specifiabilityClosureCert (K : Type*) [Nonempty K] :
  97    SpecifiabilityClosureCert K where
  98  equivalence := distinguishability_iff_nontrivial_specifiability
  99
 100end SpecifiabilityClosure
 101end Foundation
 102end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.