theorem other other

`recursor_zero`

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

formal statement (Lean)

  55theorem recursor_zero {α : Type*} (base : α) (step : α → α) :
  56    recursor base step LogicNat.zero = base := rfl

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

tick_isNNO in IndisputableMonolith.Foundation.TimeAsOrbit decl_use
tick_orbit_eq_logicNat_zero 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
categoricalMathlibCert_holds in IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib decl_use
nno_universal_existence in IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib decl_use

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
recursor in IndisputableMonolith.Foundation.UniversalForcing.Strict.CategoricalMathlib decl_use