  26    simp [boolCost, h, h']
  27
  28/-- Interpret the free step orbit in the Boolean carrier by parity. -/
  29def boolOrbitInterpret : ArithmeticFromLogic.LogicNat → Bool
  30  | ArithmeticFromLogic.LogicNat.identity => false
  31  | ArithmeticFromLogic.LogicNat.step n => Bool.not (boolOrbitInterpret n)
  32
  33/-- The discrete propositional Law-of-Logic realization. -/
  34def boolRealization : LogicRealization where
  35  Carrier := Bool
  36  Cost := Nat
  37  zeroCost := inferInstance
  38  compare := boolCost
  39  zero := false
  40  step := Bool.not
  41  Orbit := ArithmeticFromLogic.LogicNat
  42  orbitZero := ArithmeticFromLogic.LogicNat.zero
  43  orbitStep := ArithmeticFromLogic.LogicNat.succ
  44  interpret := boolOrbitInterpret
  45  interpret_zero := rfl
  46  interpret_step := by intro n; rfl
  47  orbit_no_confusion := by
  48    intro n h
  49    exact ArithmeticFromLogic.LogicNat.zero_ne_succ n h
  50  orbit_step_injective := ArithmeticFromLogic.LogicNat.succ_injective
  51  orbit_induction := by
  52    intro P h0 hs n
  53    exact ArithmeticFromLogic.LogicNat.induction (motive := P) h0 hs n
  54  orbitEquivLogicNat := Equiv.refl ArithmeticFromLogic.LogicNat
  55  orbitEquiv_zero := rfl
  56  orbitEquiv_step := by intro n; rfl
  57  identity := boolCost_self
  58  nonContradiction := boolCost_symm
  59  excludedMiddle := True

papers checked against this theorem

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