negate_toInt
plain-language theorem explainer
Negating a signed orbit and reading it as an integer equals reading first and then negating in ℤ. Anyone proving order, absolute value, or balance facts for signed orbits cites this bridge. The proof reduces both sides to integer differences of natural counts and finishes by ring.
Claim. For every signed orbit $a=(p,n)$ (intended value $p-n$), if $\mathrm{negate}(a)=(n,p)$, then the integer recovery of $\mathrm{negate}(a)$ equals the additive inverse of the integer recovery of $a$: $\mathrm{toInt}(\mathrm{negate}(a))=-\mathrm{toInt}(a)$.
background
In the primitive recognition calculus, integers are built before classical ℤ by pairing two distinction-counts. A SignedOrbit is a pair (pos, neg) of distinction naturals, with intended meaning $pos-neg$ (K4.6). The map toInt recovers the ordinary integer by casting both counts and subtracting.
Pointwise negation on signed orbits swaps the two components: $\mathrm{negate}(p,n)=(n,p)$. This is named negate rather than neg to avoid clashing with structure fields. Upstream, the same swap pattern appears for logic integers (neg on LogicInt sends $(a,b)$ to $(b,a)$) and for real protocols (interval endpoints flip sign).
The local module develops integer and rational structure on these orbit objects so later order and growth lemmas can move freely between the combinatorial representation and ordinary integer arithmetic.
proof idea
Term-mode proof. Unfold both sides via the definitions of negate and toInt: the left side is $(a.neg.toNat:\mathbb{Z})-(a.pos.toNat:\mathbb{Z})$, the right side is $-((a.pos.toNat:\mathbb{Z})-(a.neg.toNat:\mathbb{Z}))$. A single show states that equality, and ring closes the integer identity. No external lemmas beyond the definitional expansions are required.
why it matters
This is the basic commutation of signed-orbit negation with integer recovery. Downstream order theory uses it constantly: abs_negate shows absolute value is invariant under negation; balanced_negate_iff transfers balance across signs; abs_le_iff_between rewrites absolute bounds as a two-sided inequality involving negate; and several balanced-representative lemmas reduce sign cases through negate_toInt.
In the growth layer, leQ_neg_neg_iff for ratio orbits rewrites both sides with negate_toInt (together with multiplication and ofOrbit recovery) to reverse inequalities under double negation. Within Recognition Science foundation work, signed orbits are the combinatorial stand-in for integers before the forcing chain reaches continuum structure; keeping negation honest under toInt is prerequisite bookkeeping for any later comparison, mass-ladder, or cost argument that needs signed counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.