`IndisputableMonolith.Verification.Exclusivity.NontrivialityShim`

IndisputableMonolith/Verification/Exclusivity/NontrivialityShim.lean · 17 lines · 0 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Verification.Exclusivity.Framework
   3
   4namespace IndisputableMonolith
   5namespace Verification
   6namespace Exclusivity
   7
   8/-! ### Non-triviality Shim
   9
  10This module ensures the framework admits non-trivial solutions.
  11The actual non-triviality proof requires showing the framework
  12has at least two distinct physical configurations. -/
  13
  14end Exclusivity
  15end Verification
  16end IndisputableMonolith
  17

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