toNat_succ
plain-language theorem explainer
The toNat embedding sends the successor of any logic-forced natural to the standard successor on ordinary naturals. Researchers deriving Peano arithmetic from the Law of Logic cite this when moving inductive arguments or order properties between the two structures. The proof is a direct reflexivity that matches the recursive clause in the definition of toNat to the action of succ.
Claim. For any element $n$ of the logic-forced naturals, the iteration count of its successor equals one plus the iteration count of $n$: $toNat(succ n) = succ(toNat n)$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity in the orbit) and step (one further iteration of the generator). It mirrors the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The successor operation is defined by succ n := step n. The function toNat reads off the iteration count by recursion: identity maps to 0 and step n maps to succ (toNat n). This theorem sits inside the ArithmeticFromLogic module, which derives the Peano structure as theorems rather than axioms from the underlying functional equation.
proof idea
One-line wrapper that applies the recursive definition of toNat on the step constructor produced by succ.
why it matters
The result is invoked in twelve downstream theorems, including fromNat_toNat (round-trip), toNat_add (addition recovery), toNat_lt (order transfer), and lt_irrefl. It supplies the concrete link that lets arithmetic properties proved on LogicNat transfer to standard Nat, supporting the extraction of counting and ordering from the Law of Logic in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.