IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO

   1import Mathlib.CategoryTheory.Category.Basic
   2import IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib
   3
   4/-!
   5# Mathlib NNO Bridge
   6
   7This module connects the strict categorical realization to Mathlib's
   8CategoryTheory namespace. We keep the theorem content in the already proved
   9`CategoricalMathlib` recursor universal property and expose it as the
  10Mathlib-facing bridge.
  11-/
  12
  13namespace IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO
  14
  15open ArithmeticFromLogic
  16open IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib
  17
  18noncomputable section
  19
  20theorem logicNat_has_type_NNO_universal_property :
  21    ∀ {α : Type*} (base : α) (step : α → α),
  22      ∃ (f : LogicNat → α),
  23        f LogicNat.zero = base ∧
  24        ∀ n, f (LogicNat.succ n) = step (f n) :=
  25  @nno_universal_existence
  26
  27theorem logicNat_NNO_uniqueness :
  28    ∀ {α : Type*} (base : α) (step : α → α)
  29      (f g : LogicNat → α),
  30      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
  31      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
  32      f = g :=
  33  @nno_universal_uniqueness
  34
  35structure MathlibNNOCert where
  36  exists_rec :
  37    ∀ {α : Type*} (base : α) (step : α → α),
  38      ∃ (f : LogicNat → α),
  39        f LogicNat.zero = base ∧
  40        ∀ n, f (LogicNat.succ n) = step (f n)
  41  unique_rec :
  42    ∀ {α : Type*} (base : α) (step : α → α)
  43      (f g : LogicNat → α),
  44      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
  45      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
  46      f = g
  47
  48theorem mathlibNNOCert_holds : MathlibNNOCert :=
  49{ exists_rec := logicNat_has_type_NNO_universal_property
  50  unique_rec := logicNat_NNO_uniqueness }
  51
  52end
  53
  54end IndisputableMonolith.Foundation.UniversalForcing.Strict.MathlibNNO
  55