IndisputableMonolith.Foundation.UniversalForcing.DiscreteRealization

   1import IndisputableMonolith.Foundation.DiscreteLogicRealization
   2
   3/-!
   4  DiscreteRealization.lean
   5
   6  Re-export of the Boolean/propositional realization under the
   7  `Foundation.UniversalForcing` module tree.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Foundation
  12namespace UniversalForcing
  13namespace DiscreteRealization
  14
  15open DiscreteLogicRealization
  16
  17/-- Boolean/propositional Law-of-Logic realization. -/
  18def discreteRealization : LogicRealization :=
  19  boolRealization
  20
  21/-- The discrete realization carries the universal forced arithmetic. -/
  22noncomputable def discrete_arith_equiv_logicNat :
  23    (arithmeticOf discreteRealization).peano.carrier
  24      ≃ ArithmeticFromLogic.LogicNat :=
  25  discreteRealization.orbitEquivLogicNat
  26
  27end DiscreteRealization
  28end UniversalForcing
  29end Foundation
  30end IndisputableMonolith
  31