def definition def or abbrev

`logicNatFold`

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

formal statement (Lean)

  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. -/

used by (3)

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

logicNatLift in IndisputableMonolith.Foundation.ArithmeticOf decl_use
logicNat_isNNO in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
realizationOrbit_isNNO in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use

depends on (8)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
PeanoObject in IndisputableMonolith.Foundation.ArithmeticOf decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use