IndisputableMonolith.Foundation.DiscreteLogicRealization

   1import IndisputableMonolith.Foundation.UniversalForcing
   2
   3/-!
   4  DiscreteLogicRealization.lean
   5
   6  The second Law-of-Logic realization: a discrete Boolean/propositional
   7  carrier. This is the first non-continuous test case for Universal Forcing.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Foundation
  12namespace DiscreteLogicRealization
  13
  14/-- Boolean comparison cost: zero for equality, one for distinction. -/
  15def boolCost (p q : Bool) : Nat :=
  16  if p = q then 0 else 1
  17
  18@[simp] theorem boolCost_self (p : Bool) : boolCost p p = 0 := by
  19  simp [boolCost]
  20
  21theorem boolCost_symm (p q : Bool) : boolCost p q = boolCost q p := by
  22  by_cases h : p = q
  23  · subst h
  24    simp [boolCost]
  25  · have h' : q ≠ p := by intro hqp; exact h hqp.symm
  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
  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. -/
  67theorem bool_hasIdentityStep : boolRealization.hasIdentityStep :=
  68  LogicRealization.hasIdentityStep_of_nontrivial boolRealization
  69
  70/-- Boolean realization has the same forced arithmetic as every realization. -/
  71noncomputable def bool_arithmetic_invariant (R : LogicRealization.{0, 0}) :
  72    (UniversalForcing.arithmeticOf boolRealization).peano.carrier
  73      ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
  74  ArithmeticOf.equivOfInitial
  75    (UniversalForcing.arithmeticOf boolRealization) (UniversalForcing.arithmeticOf R)
  76
  77/-- The Boolean realization's forced arithmetic has the Peano surface. -/
  78theorem bool_peano_surface :
  79    ArithmeticOf.PeanoSurface (UniversalForcing.arithmeticOf boolRealization) :=
  80  UniversalForcing.peano_surface boolRealization
  81
  82end DiscreteLogicRealization
  83end Foundation
  84end IndisputableMonolith
  85