IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean

   1import IndisputableMonolith.Foundation.UniversalForcing.Strict.PositiveRatio
   2
   3/-!
   4  Strict/DiscreteBoolean.lean
   5
   6  Strict Boolean/propositional realization.  The carrier orbit is periodic,
   7  but the strict forced arithmetic is the free iteration object derived from
   8  the native generator, not the finite image inside `Bool`.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Foundation
  13namespace UniversalForcing
  14namespace Strict
  15namespace DiscreteBoolean
  16
  17open LogicAsFunctionalEquation
  18
  19def boolCost (p q : Bool) : Nat :=
  20  if p = q then 0 else 1
  21
  22@[simp] theorem boolCost_self (p : Bool) : boolCost p p = 0 := by
  23  simp [boolCost]
  24
  25theorem boolCost_symm (p q : Bool) : boolCost p q = boolCost q p := by
  26  by_cases h : p = q
  27  · subst h
  28    simp [boolCost]
  29  · have h' : q ≠ p := by intro hq; exact h hq.symm
  30    simp [boolCost, h, h']
  31
  32def xorBool (p q : Bool) : Bool :=
  33  xor p q
  34
  35/-- Strict discrete Boolean realization. -/
  36def strictBooleanRealization : StrictLogicRealization where
  37  Carrier := Bool
  38  Cost := Nat
  39  zeroCost := inferInstance
  40  compare := boolCost
  41  compose := xorBool
  42  one := false
  43  generator := true
  44  identity_law := boolCost_self
  45  non_contradiction_law := boolCost_symm
  46  excluded_middle_law := True
  47  composition_law := True
  48  invariance_law := True
  49  nontrivial_law := by
  50    simp [boolCost]
  51
  52/-- Strict Boolean forced arithmetic is canonically `LogicNat`. -/
  53def strictBoolean_arith_equiv_logicNat :
  54    (StrictLogicRealization.arith strictBooleanRealization).peano.carrier
  55      ≃ ArithmeticFromLogic.LogicNat :=
  56  (StrictLogicRealization.toLightweight strictBooleanRealization).orbitEquivLogicNat
  57
  58/-- First strict cross-realization invariance theorem:
  59positive ratios and Boolean propositions force the same arithmetic. -/
  60noncomputable def strictPositiveRatio_arith_equiv_strictBoolean
  61    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  62    (StrictLogicRealization.arith (PositiveRatio.strictPositiveRatioRealization C h)).peano.carrier
  63      ≃ (StrictLogicRealization.arith strictBooleanRealization).peano.carrier :=
  64  ArithmeticOf.equivOfInitial
  65    (StrictLogicRealization.arith (PositiveRatio.strictPositiveRatioRealization C h))
  66    (StrictLogicRealization.arith strictBooleanRealization)
  67
  68end DiscreteBoolean
  69end Strict
  70end UniversalForcing
  71end Foundation
  72end IndisputableMonolith
  73