toNat_succ
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that toNat is injective or surjective.
- Does not define or use the inverse map fromNat.
- Does not address addition, multiplication, or ordering on LogicNat.
- Does not connect to the J-cost function or the phi-ladder.
formal statement (Lean)
231@[simp] theorem toNat_succ (n : LogicNat) : toNat (succ n) = Nat.succ (toNat n) := rfl