`ArithmeticOf`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticOf
domain: Foundation
line: 65 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArithmeticOf on GitHub at line 65.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  62end PeanoObject
  63
  64/-- The arithmetic object forced by a Law-of-Logic realization. -/
  65structure ArithmeticOf (R : LogicRealization) where
  66  peano : PeanoObject
  67  initial : PeanoObject.IsInitial peano
  68
  69namespace ArithmeticOf
  70
  71/-- Peano surface of a forced arithmetic object. -/
  72structure PeanoSurface {R : LogicRealization} (A : ArithmeticOf R) : Prop where
  73  zero_ne_step : ∀ x : A.peano.carrier, A.peano.zero ≠ A.peano.step x
  74  step_injective : Function.Injective A.peano.step
  75  induction :
  76    ∀ P : A.peano.carrier → Prop,
  77      P A.peano.zero →
  78      (∀ n, P n → P (A.peano.step n)) →
  79      ∀ n, P n
  80
  81/-! ## LogicNat as the canonical initial Peano object -/
  82
  83/-- The Peano object carried by `LogicNat`. -/
  84def logicNatPeano : PeanoObject where
  85  carrier := LogicNat
  86  zero := LogicNat.zero
  87  step := LogicNat.succ
  88
  89/-- Fold from `LogicNat` into an arbitrary Peano object. -/
  90def logicNatFold (B : PeanoObject) : LogicNat → B.carrier
  91  | LogicNat.identity => B.zero
  92  | LogicNat.step n => B.step (logicNatFold B n)
  93
  94/-- Lift from `LogicNat` to any Peano object by primitive recursion. -/
  95def logicNatLift (B : PeanoObject) : PeanoObject.Hom logicNatPeano B where

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.