negate_le_negate_iff
plain-language theorem explainer
Negation reverses order on signed orbits: −b ≤ −a if and only if a ≤ b. Anyone assembling the ordered abelian group structure on the RS integer layer cites this. The proof pushes both sides across the toInt bridge and finishes with the corresponding fact on ℤ via omega.
Claim. For signed orbits $a,b$ (each a pair of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$), writing $\le$ for the internal order "$b-a$ is nonnegative" and writing $-$ for pointwise swap of the two legs, one has $-b \le -a$ if and only if $a \le b$.
background
Signed orbits are the internal integer layer of Primitive Recognition Calculus: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction-nats, read as the difference $\mathrm{pos}-\mathrm{neg}$. Negation swaps the two legs, so the intended meaning is ordinary additive inverse. The internal order is defined by nonnegativity of the difference: $a \le b$ means $b-a$ is nonnegative.
The bridge theorem le_iff_toInt_le identifies this order with the standard order on the integer image: $a \le b$ iff $a.\mathrm{toInt} \le b.\mathrm{toInt}$. Likewise, negate_toInt says the integer image of a negated orbit is the ordinary negation of the image. Together they reduce order facts about signed orbits to arithmetic on $\mathbb{Z}$.
This module builds the ordered structure on that layer (reflexivity, transitivity, totality, trichotomy, sign-flag characterizations). The present lemma is the order-reversal law for negation.
proof idea
Term-mode rewrite proof. First rewrite both sides of the biconditional with the bridge le_iff_toInt_le, so the goal becomes an inequality between integer images. Then rewrite each image with negate_toInt, obtaining $-b.\mathrm{toInt} \le -a.\mathrm{toInt}$ iff $a.\mathrm{toInt} \le b.\mathrm{toInt}$. Discharge the residual $\mathbb{Z}$ fact by omega.
why it matters
Feeds integer_order_certificate, the closure certificate that the internal signed-orbit order surface is complete (nonnegativity, flags, truncated subtraction, absolute difference, and the $\le$ display all match their integer readings). Without order-reversal under negation, the signed layer would not yet be an ordered group, and later arithmetic-from-logic constructions that treat integers as differences of distinction-nats would lack the standard comparison law. In the RS foundation stack this sits under the Primitive Recognition Calculus integer layer that eventually supports the forcing chain's discrete counting structure (eight-tick octave, rung arithmetic), not a physics identity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.