nonnegFlag_sub_iff_le
plain-language theorem explainer
For signed orbits a and b, the computable nonnegative flag on a−b is true exactly when b≤a in the internal order. Order-theory and certificate authors cite it to connect Bool flags to the Prop-level order. The proof rewrites both sides to integer inequalities via toInt and closes with omega.
Claim. For signed orbits $a,b$, the nonnegative flag of $a-b$ equals $\mathsf{true}$ if and only if $b \le a$ in the signed-orbit order (equivalently, $(a-b).\mathsf{toInt} \ge 0$).
background
Signed orbits are the internal integer model in Primitive Recognition Calculus: a pair (pos, neg) of distinction naturals, read as the difference pos − neg. Subtraction and a map toInt send them to ordinary integers.
The internal order is defined by nonnegativity of the difference: $a \le b$ means $b-a$ is nonnegative. Beside the Prop-level predicate sits a Bool flag nonnegFlag, built by structural comparison of the two sides (DistinctionNat.leq on neg vs pos). Upstream, nonnegFlag_eq_true_iff equates the flag to $0 \le z.\mathsf{toInt}$, and le_iff_toInt_le equates the order to the usual integer order on toInt.
This lemma lives in the IntegerOrder layer that packages those bridges into a closed order surface for the certificate.
proof idea
Term-mode rewrite chain, then linear arithmetic. Rewrite the left side with nonnegFlag_eq_true_iff to get $0 \le (a-b).\mathsf{toInt}$. Apply sub_toInt so the difference becomes $a.\mathsf{toInt} - b.\mathsf{toInt}$. Rewrite the right side with le_iff_toInt_le to $b.\mathsf{toInt} \le a.\mathsf{toInt}$. The two integer inequalities are identical; omega finishes.
why it matters
Closes the Bool/Prop bridge for order comparisons on signed orbits: the flag on a difference is a faithful witness of $\le$. Downstream, le_iff_nonnegFlag_sub is the swapped form used as the standard interface, and negativeFlag_sub_eq_false_iff_le derives the dual negative-flag characterization from it. Both feed the order surface that integer_order_certificate declares closed ("The internal signed-orbit order surface is closed"), via the signed nonnegative and flag display fields. In the foundation stack this is bookkeeping for arithmetic-from-logic, not a forcing-chain step (T5–T8), but it is required before integer order can be treated as fully internal and certificate-ready.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.