cmp_negate_swap
plain-language theorem explainer
Negation reverses signed-orbit order in the comparison sense: comparing −b with −a yields the same trichotomy outcome as comparing a with b. Anyone building or citing the closed integer-order surface on signed orbits needs this swap identity. The proof cases on the three values of cmp and routes each arm through the corresponding negate-order or balanced-negate lemma.
Claim. For any signed orbits $a$ and $b$, the three-way comparison of $-b$ with $-a$ equals the three-way comparison of $a$ with $b$: $\mathrm{cmp}(-b,-a)=\mathrm{cmp}(a,b)$.
background
The module develops an internal order on signed orbits, the recognition-calculus stand-in for signed integers. A signed orbit carries a magnitude together with a sign; negate flips that sign. The comparison cmp returns one of three outcomes (less, equal, greater), with equality identified with the ledger-style balanced relation on the pair.
Strict order and balance are already linked to cmp by conversion lemmas (cmp_eq_lt_iff, cmp_eq_eq_iff, cmp_eq_gt_iff). Negation interacts with those relations via negate_lt_negate_iff (order reversal under simultaneous negation) and balanced_negate_iff (balance is preserved, up to argument swap, under negation). The present identity packages those facts at the level of the trichotomous comparator itself.
Local siblings include reflexivity, totality, antisymmetry for the induced preorder, and the sign-flag characterizations of nonnegativity and negativity. Together they form the order surface later certified as closed.
proof idea
Case-split on cmp a b.
- If the outcome is
lt, convert tolt a b, applynegate_lt_negate_iffto obtainlt (-b) (-a), then re-encode ascmp (-b) (-a) = lt. - If the outcome is
eq, convert tobalanced a b, symmetrize, rewrite bybalanced_negate_iffto get balance of(-b,-a), and re-encode ascmp = eq. - If the outcome is
gt, convert tolt b a, reverse under negation, and re-encode ascmp = gt.
Each arm is a short chain of the existing iff and introduction lemmas; no new arithmetic is invented here.
why it matters
The theorem is one of the order-surface identities collected by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, absolute difference, nonnegativity, and related flags; the negate-swap law is the piece that makes comparison commute with sign flip in the expected way.
In the broader Recognition foundation this sits inside Primitive Recognition Calculus: integers and their order are not imported from Mathlib as primitives but reconstructed from distinction, balance, and signed orbits. Closing the order surface is a prerequisite for treating rung arithmetic and the phi-ladder mass formula with an internally certified integer order, rather than an external ℤ.
No forcing-chain step (T5–T8) is discharged here; the result is pure order infrastructure. It does not touch J-uniqueness, the eight-tick octave, or dimensional forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.