def definition def or abbrev

`recursor`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  51def recursor {α : Type*} (base : α) (step : α → α) : LogicNat → α
  52  | LogicNat.identity => base
  53  | LogicNat.step n => step (recursor base step n)
  54

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

tick_isNNO in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
isInitial in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
IsNaturalNumberObject in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
IsNaturalNumberObject in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
logicNat_isNNO in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
realizationOrbit_isNNO in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
metaForcedArithmeticInvariance_self in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
CategoricalMathlibCert in IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib decl_use
nno_universal_existence in IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib decl_use
recursor_succ in IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib decl_use
recursor_zero in IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib decl_use

depends on (4)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use