negativeFlag_sub_iff_lt
plain-language theorem explainer
For signed orbits a and b, the difference a−b is strictly negative (negativeFlag true) if and only if a is strictly less than b in the internal order. Order-theory and certificate authors cite it to equate the Boolean sign flag on a difference with the Prop-level strict order. The proof rewrites both sides to integer comparisons via toInt and finishes with omega.
Claim. For signed orbits $a,b$ (pairs of distinction naturals meaning $\mathrm{pos}-\mathrm{neg}$), the Boolean negative flag of the difference $a-b$ equals $\mathrm{true}$ if and only if $a<b$ in the internal strict order on signed orbits (nonnegative nonzero difference).
background
Signed orbits are the integer layer of the primitive recognition calculus: a structure SignedOrbit with fields pos and neg (distinction naturals), intended as the difference $\mathrm{pos}-\mathrm{neg}$. The Boolean negativeFlag is defined as the negation of the structural nonnegative flag, so it marks strict negativity without leaving the flag surface.
Strict order lt on signed orbits is the internal order: $a\le b$ and not balanced (equal under the balance relation). Upstream, lt_iff_toInt_lt identifies this with ordinary integer comparison of the toInt embeddings, and negativeFlag_eq_true_iff_toInt_neg says the negative flag is true exactly when toInt is negative. Subtraction is compatible with toInt via sub_toInt.
The module builds the closed integer-order surface used later by the order certificate: flags, displays, and Prop-level relations must agree.
proof idea
Term-mode rewrite chain, then omega. Rewrite the left side with negativeFlag_eq_true_iff_toInt_neg to get $(a-b).\mathrm{toInt}<0$. Replace the difference embedding by sub_toInt, so the goal is $a.\mathrm{toInt}-b.\mathrm{toInt}<0$. Rewrite the right side with lt_iff_toInt_lt to $a.\mathrm{toInt}<b.\mathrm{toInt}$. The remaining integer inequality is discharged by omega.
why it matters
Closes the bridge between the Boolean sign surface and the Prop-level strict order on differences: negativity of $a-b$ is exactly $a<b$. Downstream, lt_iff_negativeFlag_sub is the symmetric form, and both feed the integer-order certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages nonnegative and flag displays for the foundation stack.
In the Recognition forcing chain this sits under arithmetic-from-logic scaffolding for the integer layer that later supports real Cauchy structure and continuum constructions. It is not itself a T5–T8 landmark; it is bookkeeping that keeps signed-orbit order decidable and certificate-ready.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.