ofNat_toNat
plain-language theorem explainer
Converting a δ-orbit position to a verifier natural number and back recovers the original position. This is the left-inverse half of the K4.5 equivalence between the base-neutral distinction orbit and Lean Nat. Downstream factorization, injectivity, and ratio lemmas cite it directly. The proof is structural induction on the orbit, with the successor case reduced by simplification.
Claim. For every position $n$ in the base-neutral finite orbit of repeated distinction, reconstructing an orbit position from its verifier natural-number display yields $n$ again: building from the iteration count of $n$ returns $n$.
background
The module develops the primitive recognition calculus orbit: a base-neutral finite orbit of repeated distinction (K2.12), an inductive type with zero and successor. This is the δ-orbit: pure iteration count with no preferred radix.
Two maps connect the orbit to the verifier's natural numbers. The forward map reads off the iteration count (zero to 0, successor adds one). The inverse builds an orbit position by iterating successor from zero. Parallel constructions appear upstream in ArithmeticFromLogic for the logic-native natural numbers, where successor is "one more application of the generator" and the forward map "read[s] off the iteration count."
Local setting is the foundation layer that treats Peano structure as theorems of an inductive distinction process rather than axioms. The companion right-inverse identity is the sibling result; together they form the Nat equivalence.
proof idea
Structural induction on the orbit position. The zero case is definitional reflexivity under the recursive clauses of both maps. In the successor case, unfold the verifier display (toNat of a successor is Nat.succ of toNat), apply the inductive hypothesis, and simplify with the recursive clauses of ofNat and toNat. No external lemmas beyond the definitions and the orbit induction principle.
why it matters
This is half of K4.5: "the δ-orbit is equivalent to Lean Nat as a verifier display." It supplies the left_inv field of that equivalence. Downstream, display injectivity is obtained by applying the inverse map to both sides of a Nat equality and rewriting with this identity. Factorization uses it to lift Nat primality back to a δ-prime orbit ("a Nat prime display lifts back to a δ prime orbit"). Integer-rational work rewrites through it to show a ratio denominator has nonzero verifier Nat. Signed-orbit growth lemmas also discharge nonzero flags via the round trip. In the Recognition framework this seals that the distinction orbit is a faithful Peano display, so arithmetic facts on Nat transport cleanly to orbit positions without base choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.