recursor
plain-language theorem explainer
The recursor supplies the primitive recursion operator on LogicNat by direct pattern matching on its two constructors. Researchers establishing the natural-number-object property for the logic-forced arithmetic orbit cite this definition to witness the existence half of the Lawvere NNO universal property. It is realized as a direct definition that delegates to Lean's built-in inductive recursion.
Claim. Let $LogicNat$ be the inductive type generated by the constructors $identity$ and $step$. For any type $X$, element $b : X$ and map $s : X → X$, the function $r : LogicNat → X$ is defined by the equations $r(identity) = b$ and $r(step n) = s(r(n))$.
background
LogicNat is the inductive type whose constructors identity (the zero-cost multiplicative identity) and step (one iteration of the generator) realize the orbit {1, γ, γ², …} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1. The module bridges the strict categorical realization of UniversalForcing to Mathlib's CategoryTheory API, showing that LogicNat carries the algebraic content of a natural-number object in the category Type. The upstream definition of LogicNat appears in ArithmeticFromLogic and is forced directly by the Law of Logic.
proof idea
The definition is a one-line wrapper that applies Lean's built-in pattern matching on the LogicNat inductive type: the identity case returns the supplied base value and the step case applies the step function to the recursive call on the predecessor.
why it matters
This definition populates the recursor field of the IsNaturalNumberObject structure on LogicNat (see logicNat_isNNO), which is then used to prove that Tick is an NNO in TimeAsOrbit.tick_isNNO and to construct the initial object in the category of pointed endomap algebras. It supplies the recursion principle required by the Recognition Science framework for the arithmetic realization of the forcing chain, connecting the orbit generated by the logic-forced generator to the eight-tick octave and the universal property of Peano structures without reference to the standard naturals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.