recursor_succ
The successor recursion identity on LogicNat states that the primitive recursion operator applied to succ n equals the step function applied to the value on n. Categorical modelers of arithmetic within Recognition Science cite this to confirm that LogicNat satisfies the natural-number-object equations in the category of types. The proof is a direct reflexivity step from the inductive definition of the recursor on the step constructor.
claimLet $r$ denote the recursion operator on the logic-forced naturals. For any type $A$, base element $b:A$, step map $s:A→A$, and $n$ in the logic-forced naturals, $r(b,s, succ(n)) = s(r(b,s,n))$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost element) and step (one further iteration of the generator), realizing the smallest subset of positive reals closed under multiplication by the generator and containing 1. The recursor is the primitive recursion operator supplied by pattern matching on this inductive type; it is the unique function satisfying the base and successor equations. The module supplies the two commuting diagrams that transport the NNO universal property through the equivalence with ordinary naturals.
proof idea
One-line term proof that applies reflexivity directly to the defining equation of the recursor on the successor constructor of LogicNat.
why it matters in Recognition Science
Together with recursor_zero this identity is packaged into categoricalMathlibCert_holds, which certifies that LogicNat carries the NNO structure in Type. The result closes the successor square required by the NNO definition in the categorical bridge and thereby supports the arithmetic layer underlying the forcing chain T0-T8 and the phi-ladder mass formulas.
scope and limits
- Does not prove uniqueness of the mediating morphism.
- Does not construct a full category instance containing LogicNat.
- Does not extend to dependent recursion or higher-order functions.
Lean usage
theorem nno_universal_existence {α : Type*} (base : α) (step : α → α) : ∃ (f : LogicNat → α), f LogicNat.zero = base ∧ ∀ n, f (LogicNat.succ n) = step (f n) := ⟨recursor base step, recursor_zero base step, recursor_succ base step⟩formal statement (Lean)
58theorem recursor_succ {α : Type*} (base : α) (step : α → α) (n : LogicNat) :
59 recursor base step (LogicNat.succ n) = step (recursor base step n) := rfl
proof body
Term-mode proof.
60
61/-! ## NNO universal property statement
62
63In a category C with terminal object 1 and an endomorphism `s : N → N`,
64an NNO is a triple `(N, zero : 1 → N, succ : N → N)` such that for every
65`(A, base : 1 → A, step : A → A)` there is a unique morphism `f : N → A`
66with `f ∘ zero = base` and `f ∘ succ = step ∘ f`.
67
68In `Type` (the category of types), `1 = Unit` and the universal property
69becomes: for every `(A, base : Unit → A, step : A → A)` there is a unique
70`f : N → A` satisfying the obvious equations. We collapse `Unit → A` to
71just `A` (the points of A correspond bijectively to maps from `Unit`).
72-/
73
74/-- The NNO universal property on `LogicNat` in `Type`: existence. -/