lt_zero_iff_negativeFlag
plain-language theorem explainer
A signed orbit is strictly below zero exactly when its structural negative flag is true. Order and certificate lemmas cite this to swap between the internal strict order and the Boolean sign bit. The proof is a three-rewrite chain through the integer embedding of signed orbits.
Claim. For every signed orbit $z$ (difference of two distinction naturals), $z < 0$ if and only if the Boolean negative flag of $z$ equals $\mathrm{true}$.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$. The zero orbit is the balanced case. Strict order on signed orbits is defined internally as nonnegative difference with nonzero (non-balanced) difference.
The negative flag is the Boolean dual of the structural nonnegative flag: it is true precisely when nonnegativity fails. Both the order and the flag are tied to the integer embedding toInt: strict order matches ordinary $<$ on $\mathbb{Z}$, and the negative flag is true exactly when toInt is negative.
This module closes the order surface on that integer model, so flag-level and order-level statements must be interchangeable at zero.
proof idea
Three rewrites. First replace internal strict order by the integer comparison via lt_iff_toInt_lt. Second send the right-hand zero to the integer $0$ by zero_toInt. Third apply negativeFlag_eq_true_iff_toInt_neg, which already equates the negative flag with toInt z < 0. The three sides match, so the biconditional is immediate.
why it matters
Feeds the integer-order certificate that declares the signed-orbit order surface closed, and is reused by reciprocal-nonzero numerator sign lemmas that transport strict negativity across inversion. Without this bridge, Boolean sign flags and the internal $<0$ predicate would remain separate interfaces. It is pure foundation bookkeeping on the integer layer beneath rationals and Cauchy reals, not a physics forcing step (T5–T8), but it keeps the arithmetic substrate coherent for later recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.