`boolRealization`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.DiscreteLogicRealization
domain: Foundation
line: 34 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.DiscreteLogicRealization on GitHub at line 34.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  60  composition := True
  61  actionInvariant := True
  62  nontrivial := by
  63    refine ⟨true, ?_⟩
  64    simp [boolCost]

papers checked against this theorem

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