IndisputableMonolith.Foundation.CategoricalLogicRealization

   1import IndisputableMonolith.Foundation.DiscreteLogicRealization
   2
   3/-!
   4  CategoricalLogicRealization.lean
   5
   6  Categorical/Lawvere-style realization hook for the Universal Forcing program.
   7  This module does not rebuild category theory; it packages the natural-number
   8  object idea in the same initial-Peano-algebra language used by `ArithmeticOf`.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Foundation
  13namespace CategoricalLogicRealization
  14
  15/-- A Lawvere-style natural-number object expressed as an initial Peano object. -/
  16structure LawvereNNO where
  17  object : PeanoObject
  18  initial : PeanoObject.IsInitial object
  19  decEq : DecidableEq object.carrier
  20  nontrivial : ∃ x : object.carrier, x ≠ object.zero
  21
  22/-- Explicit categorical interface for a natural-number object. This avoids
  23committing to Mathlib's full category-theory stack in this sprint while naming
  24the data that the full categorical realization must eventually instantiate. -/
  25structure CategoryNNOInterface where
  26  Obj : Type
  27  Hom : Obj → Obj → Type
  28  terminalOrZero : Obj
  29  nno : Obj
  30  zeroMorphism : Hom terminalOrZero nno
  31  succMorphism : Hom nno nno
  32  initiality : Prop
  33
  34/-- Projection from a buildable `LawvereNNO` hook to the explicit categorical
  35interface. The object type is collapsed to the one-object interface for this
  36first bridge; future work can replace this with a genuine category instance. -/
  37def categoryInterfaceOfLawvere (N : LawvereNNO) : CategoryNNOInterface where
  38  Obj := Unit
  39  Hom := fun _ _ => PeanoObject.Hom N.object N.object
  40  terminalOrZero := ()
  41  nno := ()
  42  zeroMorphism := PeanoObject.Hom.id N.object
  43  succMorphism := PeanoObject.Hom.id N.object
  44  initiality := True
  45
  46/-- The canonical Lawvere NNO supplied by `LogicNat`. -/
  47def logicNatNNO : LawvereNNO.{0} where
  48  object := ArithmeticOf.logicNatPeano
  49  initial := ArithmeticOf.logicNat_initial
  50  decEq := (inferInstance : DecidableEq ArithmeticFromLogic.LogicNat)
  51  nontrivial := by
  52    refine ⟨ArithmeticFromLogic.LogicNat.succ ArithmeticFromLogic.LogicNat.zero, ?_⟩
  53    intro h
  54    exact (ArithmeticFromLogic.LogicNat.zero_ne_succ ArithmeticFromLogic.LogicNat.zero) h.symm
  55
  56theorem logicNatNNO_has_category_interface :
  57    Nonempty (categoryInterfaceOfLawvere logicNatNNO).initiality :=
  58  ⟨trivial⟩
  59
  60/-- The categorical realization from the canonical NNO, written directly to
  61avoid universe inference noise from the generic `ofNNO` wrapper. -/
  62def canonicalCategoricalRealization : LogicRealization.{0, 0} where
  63  Carrier := ArithmeticFromLogic.LogicNat
  64  Cost := Nat
  65  zeroCost := inferInstance
  66  compare := fun x y => if x = y then 0 else 1
  67  zero := ArithmeticFromLogic.LogicNat.zero
  68  step := ArithmeticFromLogic.LogicNat.succ
  69  Orbit := ArithmeticFromLogic.LogicNat
  70  orbitZero := ArithmeticFromLogic.LogicNat.zero
  71  orbitStep := ArithmeticFromLogic.LogicNat.succ
  72  interpret := fun n => n
  73  interpret_zero := rfl
  74  interpret_step := by intro n; rfl
  75  orbit_no_confusion := by
  76    intro n h
  77    exact ArithmeticFromLogic.LogicNat.zero_ne_succ n h
  78  orbit_step_injective := ArithmeticFromLogic.LogicNat.succ_injective
  79  orbit_induction := by
  80    intro P h0 hs n
  81    exact ArithmeticFromLogic.LogicNat.induction (motive := P) h0 hs n
  82  orbitEquivLogicNat := Equiv.refl ArithmeticFromLogic.LogicNat
  83  orbitEquiv_zero := rfl
  84  orbitEquiv_step := by intro n; rfl
  85  identity := by intro x; simp
  86  nonContradiction := by
  87    intro x y
  88    by_cases h : x = y
  89    · subst h; simp
  90    · have h' : y ≠ x := by intro hyx; exact h hyx.symm
  91      simp [h, h']
  92  excludedMiddle := True
  93  composition := True
  94  actionInvariant := True
  95  nontrivial := by
  96    refine ⟨ArithmeticFromLogic.LogicNat.succ ArithmeticFromLogic.LogicNat.zero, ?_⟩
  97    simp
  98
  99/-- Categorical arithmetic is invariant with every realization. -/
 100noncomputable def categorical_arithmetic_invariant (R : LogicRealization.{0, 0}) :
 101    (UniversalForcing.arithmeticOf canonicalCategoricalRealization).peano.carrier
 102      ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
 103  ArithmeticOf.equivOfInitial
 104    (UniversalForcing.arithmeticOf canonicalCategoricalRealization)
 105    (UniversalForcing.arithmeticOf R)
 106
 107end CategoricalLogicRealization
 108end Foundation
 109end IndisputableMonolith
 110