negativeFlag_eq_true_iff_nonnegFlag_eq_false
plain-language theorem explainer
For any signed orbit difference, the strict-negativity Boolean is true exactly when the structural nonnegative flag is false. Sign, order, and multiplication lemmas in the primitive recognition integer layer cite this equivalence constantly. The proof is a two-line unfold-and-cases argument from the definition of negativity as Boolean negation of the nonnegative flag.
Claim. For every signed orbit $z$ (a pair of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), the strict-negativity flag of $z$ equals $\mathsf{true}$ if and only if the nonnegative flag of $z$ equals $\mathsf{false}$.
background
A signed orbit is the primitive integer carrier in this layer: a pair of distinction naturals (pos, neg) with intended meaning $\mathrm{pos}-\mathrm{neg}$. Order and sign are not imported from Int; they are rebuilt from structural comparison of the two sides.
The nonnegative flag is the computable Boolean DistinctionNat.leq z.neg z.pos: true precisely when the negative side is at most the positive side. Strict negativity is defined, not axiomatized, as failure of that flag: negativeFlag z := !z.nonnegFlag. The doc-comment states this explicitly: "Strict negativity as failure of the structural nonnegative flag."
This module develops the internal signed-orbit order surface (reflexivity, totality, trichotomy, zero comparisons). The present fact is the Boolean exclusivity link between the two sign flags before those order lemmas are stated.
proof idea
One short tactic proof. Unfold the definition of the negativity flag to expose Boolean negation of the nonnegative flag. Case-split on the two values of z.nonnegFlag; each branch is discharged by simp on Boolean equality. No external lemmas are required beyond the definitional unfolding.
why it matters
This is the basic exclusivity bridge between the two sign Booleans. Downstream it is used throughout the integer-order development: zero and strict-zero characterizations, multiplication sign rules (negativeFlag_mul_eq_false_of_balanced_zero_left/right, nonnegFlag_mul_iff_not_strict_opposite_sign), and reciprocal numerator identities (recipNonzero_num_nonnegFlag_eq, recipNonzero_num_abs_eq_den, balanced product lemmas).
It also feeds the closed certificate integer_order_certificate, whose fields package the signed nonnegative displays that the rest of the foundation treats as the finished integer-order surface. In the Recognition stack this sits under the primitive recognition calculus that eventually supports the forcing chain's discrete arithmetic, not under T5–T8 themselves; it is infrastructure so that later phi-ladder and mass bookkeeping can treat signed comparison as proved rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.