toInt_eq
plain-language theorem explainer
Unfolds the integer recovery map on a signed orbit to the plain difference of its positive and negative Nat counts. Cited by the choice-free order bridge that equates signed-orbit order with ordinary integer order. Proof is a one-line case split that applies the constructor form of the recovery map.
Claim. For every signed orbit $a$, the recovered integer equals the difference of the natural numbers read from its positive and negative parts: $\mathrm{toInt}(a) = (\mathrm{toNat}(a_+) : \mathbb{Z}) - (\mathrm{toNat}(a_-) : \mathbb{Z})$.
background
In the primitive recognition calculus, integers are recovered from logic-level pairs of natural numbers (positive and negative legs). A signed orbit packages those two legs; the recovery map toInt sends the pair to an ordinary integer by subtracting the Nat counts of the two legs.
Upstream, IntegersFromLogic.toInt_mk states exactly that constructor identity: for logic naturals $a,b$, $\mathrm{toInt}(\mathrm{mk},a,b) = (\mathrm{toNat},a) - (\mathrm{toNat},b)$. The Nat extraction toNat itself is the forward iteration-count map from logic naturals. The present lemma simply specializes that constructor identity to the signed-orbit carrier.
The surrounding module builds a choice-free order theory for ratio orbits and signed orbits, deliberately avoiding any path that would reintroduce classical choice into the integer comparison.
proof idea
Case-split on the signed-orbit constructor. On the mk pos neg case, the goal is definitionally the statement of SignedOrbit.toInt_mk pos neg (the signed-orbit packaging of the upstream toInt_mk identity), so the proof closes by that lemma.
why it matters
This is a private bookkeeping step inside the choice-free integer-order bridge. Its sole consumer is le_iff_toInt_le_cf, whose doc-comment states the design constraint: route the order equivalence through the choice-free Nat bridge le_iff_toNat_cf and never through the choice-tainted SignedOrbit.le_iff_toInt_le.
By rewriting both sides of the order comparison as explicit Nat-cast differences, the parent lemma can finish with elementary omega arithmetic. That keeps the Grow-layer monotonicity and order facts (including additive monotonicity of the ratio-orbit order) inside the choice-free fragment of the foundation stack, which is required before later forcing-chain and recognition-calculus results can treat integer comparisons as pure constructive data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.