toNat_fromNat
The round-trip equality shows that the embedding of ordinary naturals into the logic-forced naturals is inverted by the extraction map. Developers of the Recognition Science arithmetic layer cite it when verifying faithful recovery of Peano structure from the functional equation. The argument proceeds by induction on the input natural number, reducing the successor case via the commutation rules for the step operation.
claimFor every natural number $n$, if $f$ embeds $n$ into the logic-forced naturals by iterated successor from the identity element and $t$ extracts the step count, then $t(f(n)) = n$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost base element) and step (one application of the generator), mirroring the smallest multiplicative orbit containing 1. The map fromNat builds an element of LogicNat by recursing on the step constructor; toNat is the inverse extraction that returns the number of steps taken. The module derives these maps directly from the Law of Logic without external axioms on arithmetic.
proof idea
The proof applies induction on the natural number n. The zero case holds by reflexivity. The successor case unfolds the successor commutation lemmas for fromNat and toNat, then applies the induction hypothesis.
why it matters in Recognition Science
This supplies the right inverse for the equivalence equivNat between LogicNat and Nat. It is used downstream to transport statements about integers, modular interpretations, and prime ledger atoms. The result closes the recovery of standard natural-number arithmetic inside the structure forced by the functional equation, enabling the later construction of integers from logic.
scope and limits
- Does not establish the left inverse fromNat to toNat.
- Does not define or prove properties of addition on LogicNat.
- Does not address ordering or inequalities.
- Does not extend the recovery to integers or reals.
formal statement (Lean)
243theorem toNat_fromNat : ∀ n : Nat, toNat (fromNat n) = n := by
proof body
Term-mode proof.
244 intro n
245 induction n with
246 | zero => rfl
247 | succ n ih =>
248 show toNat (fromNat (Nat.succ n)) = Nat.succ n
249 rw [fromNat_succ, toNat_succ, ih]
250
251/-- **Recovery theorem (carrier)**: `LogicNat` and `Nat` have the same
252underlying set, witnessed by the round-trip equalities. -/