fromNat_succ
plain-language theorem explainer
The theorem shows that the embedding of natural numbers into the LogicNat structure commutes with the successor operation. Researchers building Peano arithmetic as theorems from the Recognition Science functional equation would cite this compatibility. The proof is immediate by reflexivity because the recursive clause of fromNat on successor matches the definition of succ exactly.
Claim. For every natural number $n$, the embedding fromNat applied to $n+1$ equals the successor of the embedding applied to $n$, where fromNat sends $0$ to the identity element and iterates the step generator, while successor applies one step.
background
In ArithmeticFromLogic the type LogicNat is generated from an identity element by repeated application of a step operation extracted from the underlying functional equation. The map fromNat is defined recursively by sending zero to the identity and the successor of any $n$ to the step applied to fromNat $n$. The successor operation on LogicNat is defined simply as applying one step to its argument.
proof idea
The proof is a one-line wrapper that applies reflexivity. The recursive clause in the definition of fromNat on Nat.succ n unfolds directly to the step of fromNat n, which is identical to the definition of succ applied to fromNat n.
why it matters
This result is invoked by the round-trip theorems fromNat_toNat and toNat_fromNat that establish the isomorphism between Nat and LogicNat. It supplies the successor compatibility required to derive the Peano axioms as theorems inside the Recognition Science framework rather than as independent postulates, consistent with the forcing chain that obtains arithmetic from the J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.