negativeFlag_negate_ofOrbit_eq_true_iff_ne_zero
plain-language theorem explainer
Negating the signed-orbit embedding of a distinction natural n is strictly negative exactly when n is nonzero. Order and certificate authors cite this to equate the Boolean negative flag on −ofOrbit(n) with n ≠ 0. The proof is a two-direction constructor: the forward arm rewrites through toInt and collapses at zero by norm_num; the reverse arm applies the already-proved one-sided lemma.
Claim. For every distinction natural $n$, the signed orbit obtained by embedding $n$ and then pointwise negating it has negative flag equal to true if and only if $n \neq 0$.
background
In the primitive recognition calculus, integers are realized as signed orbits: pairs of distinction naturals (pos, neg) with integer value toInt = pos.toNat − neg.toNat. The map ofOrbit embeds a distinction natural $n$ as the nonnegative orbit with that magnitude. Pointwise negate swaps the two components, so negate_toInt gives (negate a).toInt = −a.toInt.
Strict negativity is the Boolean negativeFlag, defined as the failure of the structural nonnegative flag. Upstream, negativeFlag_eq_true_iff_toInt_neg equates that flag with toInt < 0. The one-sided companion negativeFlag_negate_ofOrbit_of_ne_zero already shows that for $n \neq 0$ the negated embedding is negative. This module builds the internal order on signed orbits used by the integer-order certificate.
proof idea
Term-mode constructor splits the biconditional.
Forward: assume the negative flag is true and $n = 0$. Rewrite the hypothesis with $n = 0$, then chain negativeFlag_eq_true_iff_toInt_neg, negate_toInt, ofOrbit_toInt, and toNat_zero to obtain a numeric falsehood (0 < 0 shape), discharged by norm_num.
Reverse: apply the existing lemma negativeFlag_negate_ofOrbit_of_ne_zero at $n$ and the nonzero hypothesis.
why it matters
Feeds integer_order_certificate, which closes the internal signed-orbit order surface (nonnegativity displays, flag equivalences, and related order facts). Without the iff, the certificate cannot treat “−ofOrbit(n) is negative” as interchangeable with “n is a positive distinction natural.”
In the Recognition foundation stack this sits under arithmetic-from-logic: distinction naturals and signed orbits are the carrier before rationals and the J-cost calculus. It is pure order bookkeeping, not a forcing-chain step (T5–T8), but it is required scaffolding so later mass-ladder and constant extractions can rely on a closed integer order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.