toNat_fromNat
plain-language theorem explainer
The embedding of ordinary natural numbers into the logic orbit and the projection back form a round-trip identity. Researchers deriving Peano arithmetic inside the Recognition Science functional equation cite this to confirm the structures coincide exactly. The argument is induction on the input number, reducing the successor case via commutation of the two maps.
Claim. For every natural number $n$, if $f$ embeds $n$ into the orbit generated by iterated application of the logic step and $g$ is the recovery projection, then $g(f(n)) = n$.
background
LogicNat is the inductive type with constructors identity (zero-cost element) and step, representing the smallest subset of positive reals closed under multiplication by the generator and containing 1, as forced by the Law of Logic. The map fromNat builds the corresponding LogicNat element by recursion: identity at zero and one application of step at each successor. toNat is the inverse projection that recovers the original count. The module ArithmeticFromLogic derives the full arithmetic structure (including successor, addition, and order) as theorems from the Recognition Composition Law rather than as axioms. Upstream, fromNat_succ states that fromNat commutes with successor, and the inductive definition of LogicNat supplies the orbit structure.
proof idea
The proof is by induction on the natural number n. The base case at zero is reflexivity. The successor case rewrites the left-hand side using the commutation lemmas fromNat_succ and toNat_succ, then applies the induction hypothesis to obtain the right-hand side.
why it matters
This recovery supplies the right inverse for the equivalence equivNat that identifies LogicNat with ordinary Nat. It is invoked in fromInt_toInt and toInt_fromInt when lifting the bijection to integers, in modular_interpret_periodic to transfer periodicity, and in one_not_primeLedgerAtomLogic to move primality statements between the two representations. The result closes the bijection step in the foundation layer that embeds standard arithmetic inside the orbit derived from the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.