recursor_succ
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.