lt_iff_nonnegFlag_sub_eq_false
plain-language theorem explainer
Strict order on signed orbits is equivalent to the nonnegative flag of their difference evaluating to false. Anyone wiring the integer-order certificate or bridging Bool flags to Prop-level comparison cites this. The proof is a one-line symmetry of the already-proved converse biconditional.
Claim. For signed orbits $a$ and $b$, one has $a < b$ if and only if the computable nonnegative flag of the difference $a-b$ equals $\mathsf{false}$.
background
A signed orbit is a pair of distinction-nat sides (pos, neg), read as the difference pos - neg. Its computable nonnegative flag is the structural Boolean leq neg pos: true precisely when the negative side does not exceed the positive side.
Strict order on signed orbits is the internal Prop le a b ∧ ¬ balanced a b (nonnegative difference that is not a balanced zero). The sibling theorem nonnegFlag_sub_eq_false_iff_lt already equates failure of that flag on a - b with a < b, by rewriting through the integer embedding and discharging the comparison with omega.
This module builds the order surface for the primitive recognition calculus integers: flags, balance, and Prop-level lt/le must agree before the certificate can close.
proof idea
One-line term wrapper: take the converse biconditional nonnegFlag_sub_eq_eq_false_iff_lt a b and apply Iff.symm. No new rewriting or case analysis is introduced 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, leq, absolute difference, and both Prop and Bool forms of nonnegativity; this direction of the flag/lt bridge is the orientation needed when a proof starts from the Prop-level order and must discharge a Boolean goal (or the reverse).
In the foundation layer this is bookkeeping, not a forcing-chain step: it makes the integer order assembled from recognition primitives interchangeable with its computable flag presentation, so later PRC constructions (rationals, Cauchy reals) can inherit a coherent strict order without dual APIs drifting apart.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.