IndisputableMonolith.Foundation.UniversalForcing.Strict.Categorical

   1import IndisputableMonolith.Foundation.UniversalForcing.Strict.Modular
   2import IndisputableMonolith.Foundation.CategoricalLogicRealization
   3
   4/-!
   5  Strict/Categorical.lean
   6
   7  Strict categorical/Lawvere-style realization hook. The carrier is the
   8  canonical `LogicNat` NNO surface from `CategoricalLogicRealization`; future
   9  work can refine this to Mathlib's full category-theory NNO API.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace UniversalForcing
  15namespace Strict
  16namespace Categorical
  17
  18open ArithmeticFromLogic
  19
  20def logicNatCost (a b : LogicNat) : Nat :=
  21  if a = b then 0 else 1
  22
  23@[simp] theorem logicNatCost_self (a : LogicNat) : logicNatCost a a = 0 := by
  24  simp [logicNatCost]
  25
  26theorem logicNatCost_symm (a b : LogicNat) : logicNatCost a b = logicNatCost b a := by
  27  by_cases h : a = b
  28  · subst h
  29    simp [logicNatCost]
  30  · have h' : b ≠ a := by intro hb; exact h hb.symm
  31    simp [logicNatCost, h, h']
  32
  33/-- Strict categorical realization via the canonical `LogicNat` Peano/NNO hook. -/
  34def strictCategoricalRealization : StrictLogicRealization where
  35  Carrier := LogicNat
  36  Cost := Nat
  37  zeroCost := inferInstance
  38  compare := logicNatCost
  39  compose := fun a b => a + b
  40  one := LogicNat.zero
  41  generator := LogicNat.succ LogicNat.zero
  42  identity_law := logicNatCost_self
  43  non_contradiction_law := logicNatCost_symm
  44  excluded_middle_law := True
  45  composition_law := True
  46  invariance_law := True
  47  nontrivial_law := by
  48    simp [logicNatCost, LogicNat.zero_ne_succ]
  49
  50def strictCategorical_arith_equiv_logicNat :
  51    (StrictLogicRealization.arith strictCategoricalRealization).peano.carrier
  52      ≃ LogicNat :=
  53  (StrictLogicRealization.toLightweight strictCategoricalRealization).orbitEquivLogicNat
  54
  55end Categorical
  56end Strict
  57end UniversalForcing
  58end Foundation
  59end IndisputableMonolith
  60