toNat_add
plain-language theorem explainer
Orbit addition on distinction naturals is compatible with ordinary Nat addition under the verifier display map. Anyone recovering Peano arithmetic from recognition orbits cites this as the addition recovery step (K4.5). The proof inducts on the second summand, rewrites via the zero and successor equations for orbit addition and the display lemmas, then closes the Nat identity with omega.
Claim. For distinction naturals $a$ and $b$, the verifier display of their orbit sum equals the sum of their displays: $\mathrm{display}(a+b)=\mathrm{display}(a)+\mathrm{display}(b)$, where display reads the orbit iteration count as a Lean natural number.
background
In the primitive recognition calculus, distinction naturals are orbit positions generated by iterated recognition steps. Addition is defined on those orbits (zero and successor clauses), not postulated as a Peano primitive. The verifier display map sends each orbit position to the Lean natural that counts how many generator steps separate it from the identity.
The sibling module ArithmeticFromLogic develops the same story for logic naturals: successor is one more application of the generator, and toNat is the forward map that reads off the iteration count. Its recovery theorem already states that logic-natural addition agrees with Nat addition under that equivalence. OrbitArithmetic ports the same recovery to distinction orbits.
Local lemmas used here are the orbit addition equations for zero and successor, plus the display identities for zero and successor (display of successor is Nat.succ of the display).
proof idea
Induction on the second summand $b$.
Zero case: rewrite orbit addition at zero (add_zero_eq), display of zero, and Nat.add_zero.
Successor case: the goal is rewritten to display of succ(a+n) versus display of $a$ plus display of succ n. Apply the display-of-successor identity on both sides, insert the inductive hypothesis, and finish the remaining Nat equality with omega.
why it matters
This is K4.5: verifier display of orbit addition matches Lean Nat addition. It is the addition half of the recovery isomorphism that lets Peano facts transfer from Nat back to distinction orbits.
Downstream it is the cast step inside left cancellation (equal sums imply equal summands after display, then injectivity returns), antisymmetry of the induced order, irreflexivity of strict order, the order-recovery equivalence, multiplication recovery, and the integer addition construction in IntegersFromLogic. Without it, every cancellation or order argument would have to re-induct on the orbit definition instead of quoting Nat arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.