lt_iff_negativeFlag_sub
plain-language theorem explainer
For signed orbits, a is strictly less than b exactly when the difference a − b carries the negative flag. Order theorists and anyone wiring the PRC integer layer cite this to flip between relational order and the Boolean sign surface. The proof is a one-line symmetry of the reverse biconditional.
Claim. For signed orbits $a,b$ (each a pair of distinction-natural positions meaning $\mathrm{pos}-\mathrm{neg}$), one has $a < b$ if and only if the signed difference $a-b$ has negative flag equal to true. Here $<$ is the internal strict order (nonnegative difference and not balanced), and the negative flag is the Boolean negation of the structural nonnegative flag.
background
Signed orbits are the PRC integer layer: a structure SignedOrbit with fields pos and neg of distinction-natural type, intended as the difference $\mathrm{pos}-\mathrm{neg}$. The internal strict order on signed orbits is defined as $a \le b$ together with failure of balance (nonnegative difference that is not zero in the balanced sense). The negative flag on a signed orbit is the Boolean negation of its structural nonnegative flag, so it marks strict negativity without leaving the flag surface.
The companion lemma negativeFlag_sub_iff_lt already equates “$(a-b)$ has negative flag true” with “$a < b$”, by reducing both sides through the integer embedding (toInt) and discharging the resulting arithmetic with omega. The present statement is the converse orientation of that same biconditional, kept as a named fact so downstream certificate code can quote either direction cleanly.
Local setting is the IntegerOrder module of Primitive Recognition Calculus: closing the order surface on signed orbits so that relational comparisons, Boolean flags, and the integer embedding all agree.
proof idea
One-line term proof: apply symmetry of the already-proved biconditional negativeFlag_sub_iff_lt a b. That upstream lemma rewrites the negative-flag side via negativeFlag_eq_true_iff_toInt_neg and the subtraction identity sub_toInt, rewrites the order side via lt_iff_toInt_lt, then finishes by omega on the embedded integers. No new arithmetic is done here.
why it matters
Feeds integer_order_certificate, whose doc-comment states that “the internal signed-orbit order surface is closed.” That certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, signed nonnegativity, and the nonnegative flag; the present iff supplies the matching strict-order / negative-flag bridge so the certificate can treat relational $<$ and the Boolean sign surface as interchangeable.
In the Recognition foundation stack this sits under Arithmetic-from-Logic and the PRC integer/rational ladder: once signed-orbit order is flag-complete, later real-Cauchy and ratio-orbit constructions inherit a coherent strict order without re-proving sign bookkeeping. It is not itself a forcing-chain step (T5–T8), but it is infrastructure those later layers assume when they speak of ordered differences on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.