toNat
plain-language theorem explainer
The recursive map from LogicNat to standard naturals counts the number of step applications starting from the identity constructor. Researchers embedding Peano arithmetic into the orbit generated by the Law of Logic cite this when moving cancellation and induction results between the two representations. The definition is a direct pattern match that unfolds the inductive structure without invoking external lemmas.
Claim. The forward map from the logic natural numbers to the standard naturals is given by recursion: the identity element maps to zero and each application of the step constructor maps to the successor of the image of its argument.
background
LogicNat is the inductive type forced by the Law of Logic, with constructors identity (the zero-cost multiplicative identity) and step (one further iteration of the generator). This structure encodes the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The successor operation on LogicNat is the direct application of the step constructor.
proof idea
The definition is a direct recursive pattern match on the two constructors of LogicNat. Identity is sent to zero in the standard naturals; each step is sent to the successor of the recursive image of its argument. No lemmas or tactics are applied; the recursion itself supplies the iteration count.
why it matters
This map supplies the bridge that lets arithmetic theorems proved in the standard naturals be transferred to the logic-derived naturals, as seen in the left-cancellation result for addition. It supports downstream work on phi-powers in the algebra module and on lattice-energy proxies in chemistry. Within the Recognition framework it completes the derivation of basic arithmetic from the functional equation without positing Peano axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.