pith. machine review for the scientific record. sign in
def definition def or abbrev

boolRealization

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  34def boolRealization : LogicRealization where
  35  Carrier := Bool

proof body

Definition body.

  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
  60  composition := True
  61  actionInvariant := True
  62  nontrivial := by
  63    refine ⟨true, ?_⟩
  64    simp [boolCost]
  65
  66/-- The discrete realization has a non-trivial identity-step shadow. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (22)

Lean names referenced from this declaration's body.