fromNat_toNat
The round-trip equality shows that the iteration-count map toNat is left-inverted by the orbit-construction map fromNat on the logic-forced naturals. Researchers deriving arithmetic operations or embeddings from the functional equation cite it to justify routing equalities through ordinary Nat. The argument is a direct induction on the two-constructor inductive type, reducing the successor case via the commutation lemmas fromNat_succ and toNat_succ.
claimFor every element $n$ of the naturals forced by the law of logic, the orbit-construction map recovers $n$ exactly when applied to the iteration count of $n$: $fromNat(toNat n) = n$.
background
The module constructs arithmetic directly from the functional equation by defining LogicNat as an inductive type whose constructors are the zero-cost identity element and the successor obtained by one more application of the generator. This encodes the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the self-similar fixed point and containing 1. The maps toNat and fromNat are introduced after the Peano axioms have been derived as theorems from this inductive structure; toNat extracts the number of successor steps while fromNat rebuilds the element by iterated application of successor.
proof idea
The proof proceeds by induction on the inductive structure of LogicNat. The identity base case holds by reflexivity. In the successor case the goal is rewritten by the commutation theorems toNat_succ and fromNat_succ, after which the induction hypothesis applies directly.
why it matters in Recognition Science
This left-inverse property supplies the left_inv field of the equivalence equivNat, which in turn enables the transfer principles eq_iff_toNat_eq and add_left_cancel used throughout the arithmetic development. It also feeds embed_injective and the order lemmas le_antisymm and toNat_le. The declaration therefore completes the bridge from the abstract logic naturals to concrete Nat, a prerequisite for integer arithmetic, the mass ladder, and the embedding of distinct powers of the generator.
scope and limits
- Does not establish the right inverse toNat (fromNat k) = k.
- Does not define addition or the order relation on LogicNat.
- Does not address the embedding of LogicNat into the positive reals.
- Does not prove uniqueness of the isomorphism with ordinary naturals.
Lean usage
def equivNat : LogicNat ≃ Nat where toFun := toNat invFun := fromNat left_inv := fromNat_toNat right_inv := toNat_fromNatformal statement (Lean)
235theorem fromNat_toNat : ∀ n : LogicNat, fromNat (toNat n) = n := by
proof body
Term-mode proof.
236 intro n
237 induction n with
238 | identity => rfl
239 | step n ih =>
240 show fromNat (toNat (succ n)) = succ n
241 rw [toNat_succ, fromNat_succ, ih]
242