toInt_mk
plain-language theorem explainer
Unfolding the integer recovery map on a signed orbit pair yields the difference of the two natural counts. Anyone proving that signed-orbit arithmetic matches ordinary integer arithmetic cites this simp lemma. The proof is pure reflexivity: the map is defined as that difference.
Claim. For any distinction naturals $a$ and $b$, the integer recovered from the signed orbit $\langle a,b\rangle$ equals $(\mathrm{toNat}\,a)-(\mathrm{toNat}\,b)$ in $\mathbb{Z}$.
background
In the primitive recognition calculus, integers are realized as signed differences of orbits. A signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, with intended meaning $\mathrm{pos}-\mathrm{neg}$ (K4.6). Distinction naturals expose a forward map that reads off the iteration count of the underlying constructive natural.
The recovery map sending a signed orbit to an ordinary integer is the direct analogue of the LogicInt-to-Int recovery in IntegersFromLogic. Upstream, that recovery is a quotient lift of the core difference of natural counts, and the parallel constructor lemma already records that the class of $(a,b)$ maps to $\mathrm{toNat},a-\mathrm{toNat},b$. The present statement is the same identity at the raw structure level used by the recognition calculus.
proof idea
One-line reflexivity. On a structure value $\langle a,b\rangle$, the recovery map is definitionally the cast difference $(a.\mathrm{toNat}:\mathbb{Z})-(b.\mathrm{toNat}:\mathbb{Z})$, so rfl closes the goal. The lemma is marked @[simp], so downstream rewrites fire without manual unfolding.
why it matters
This is the computational interface between signed orbits and ordinary integers. Downstream results that treat the recovery map as a ring homomorphism (preservation of addition, multiplication, and negation) and the round-trips with the inverse construction all unfold constructors through this simp rule or its LogicInt twin. In the Recognition foundation stack it sits under the arithmetic-from-logic layer that supplies discrete counting for later forcing-chain landmarks (eight-tick octave, rung indices on the $\phi$-ladder). Without a clean constructor unfolding, every integer identity on orbits would re-expand the recovery map by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.