negativeFlag_eq_true_iff_toInt_neg
plain-language theorem explainer
For a signed orbit z (difference of two distinction naturals), the Boolean negativity flag is true exactly when the integer display of z is strictly negative. Order and multiplication lemmas in IntegerOrder cite this bridge constantly. The proof cases on the nonnegative flag and rewrites through its existing true/false characterizations, finishing with omega.
Claim. Let $z$ be a signed orbit (a pair of distinction naturals interpreted as $\mathrm{pos}-\mathrm{neg}$). Then the structural negativity flag of $z$ equals $\mathsf{true}$ if and only if the integer recovery map applied to $z$ satisfies $z_{\mathbb{Z}} < 0$.
background
In the Primitive Recognition Calculus, integers are not primitive: they arise as signed orbit differences. A SignedOrbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, with intended meaning $\mathrm{pos}-\mathrm{neg}$. The recovery map toInt sends such a pair to an ordinary integer (via the LogicInt quotient and its display).
Nonnegativity is decided structurally by a Boolean nonnegFlag. The negativity flag is defined simply as its Boolean negation: strict negativity is failure of structural nonnegativity. Prior lemmas already equate nonnegFlag = true with toInt ≥ 0 and nonnegFlag = false with toInt < 0.
This module sits in the foundation layer that reconstructs integer arithmetic and order from recognition orbits, before higher analytic or physical layers attach.
proof idea
Unfold the definition of the negativity flag as Boolean not of the nonnegative flag. Case on whether nonnegFlag is true.
If it is true, rewrite and simplify; the nonnegative-true characterization gives toInt ≥ 0, so toInt < 0 is false, and omega closes the biconditional.
If it is not true, force nonnegFlag = false by exhaustive cases on the Boolean, rewrite, simplify, and apply the nonnegative-false characterization, which is exactly toInt < 0.
why it matters
This is the Boolean-to-integer bridge for strict negativity on signed orbits. Downstream IntegerOrder results depend on it heavily: absolute value identities (abs_toInt_of_negativeFlag), left/right multiplication comparison reversals under a negative factor (cmp_mul_*_of_negativeFlag, le_mul_*_iff_of_negativeFlag, lt_mul_*_iff_of_negativeFlag), and the zero-order characterization lt_zero_iff_negativeFlag.
Without this equivalence, structural flags and the integer display would drift apart, blocking ordered-ring reasoning on recognition-built integers. It is pure foundation plumbing (not a T0–T8 forcing step), but it is load-bearing for every later inequality that multiplies by a negative signed orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.