negate_lt_negate_iff
plain-language theorem explainer
Negation reverses strict order on signed orbits: −b < −a if and only if a < b. Anyone assembling the integer comparison layer from Recognition primitives, or proving that signed-orbit cmp is compatible with negation, cites this. The proof rewrites both sides through the toInt bridge, applies the negation-to-integer identity, and closes with omega on the classical law −y < −x ↔ x < y.
Claim. For signed orbits $a,b$ (pairs of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), writing $-$ for component swap, one has $(-b)<(-a)$ if and only if $a<b$, where $<$ is the internal strict order (nonnegative difference that is not balanced).
background
Signed orbits are the K4.6 integer model in Primitive Recognition Calculus: a structure with two distinction-natural components, intended as $\mathrm{pos}-\mathrm{neg}$. Negation swaps those components (named negate to avoid clashing with structure fields). The internal strict order is nonnegative difference that is not balanced equality.
The bridge theorem lt_iff_toInt_lt identifies that order with ordinary integer comparison of the derived toInt values. Separately, negate_toInt states that the integer image of a negated orbit is the ordinary additive inverse. Upstream, LogicNat strict order is the usual successor-difference existence predicate; here the work is entirely on the signed-orbit surface.
Local setting is the IntegerOrder module, which packages order laws, sign flags, and trichotomy for the certificate that the signed-orbit order surface is closed.
proof idea
Term-style tactic proof in three steps. First rewrite both occurrences of signed-orbit strict order via lt_iff_toInt_lt, so the goal becomes an ordinary integer comparison of toInt images. Second rewrite both sides with negate_toInt, replacing (negate b).toInt and (negate a).toInt by -b.toInt and -a.toInt. Third, omega discharges the classical integer fact $-y < -x \leftrightarrow x < y$. No induction and no case split on signs.
why it matters
Feeds cmp_negate_swap, which lifts the same reversal from strict order to the three-way comparison function on signed orbits (the lt branch of that proof invokes this iff). Also listed among the supporting facts for integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition stack this is bookkeeping on the arithmetic layer beneath the forcing chain, not a T0–T8 landmark itself. It ensures the integer model built from distinction orbits behaves like $\mathbb{Z}$ under negation, so later mass-ladder and cost constructions can treat signed differences without ad-hoc sign cases. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.