nonnegFlag_sub_eq_false_iff_lt
plain-language theorem explainer
For signed orbits, the structural nonnegative flag of a−b is false exactly when a is strictly less than b. Order theorists building integers from recognition primitives cite this to connect the Boolean flag to the internal strict order. The proof rewrites both sides to integer comparisons via toInt and finishes by omega.
Claim. For signed orbits $a,b$ (pairs of distinction-nats meaning $\mathrm{pos}-\mathrm{neg}$), the computable nonnegative flag of the difference $a-b$ equals false if and only if $a<b$ in the internal strict order (nonnegative nonzero difference).
background
Signed orbits are the integer layer of Primitive Recognition Calculus: a structure with two DistinctionNat sides, read as $\mathrm{pos}-\mathrm{neg}$. The map toInt sends each signed orbit to an ordinary integer. Strict order on signed orbits is defined internally as the weak order plus failure of balance (equal sides after cancellation), equivalently $a.\mathrm{toInt}<b.\mathrm{toInt}$.
The nonnegative flag is a Boolean computed by structural comparison of the two sides (leq of neg against pos). Upstream, that flag is false exactly when the integer value is negative. Subtraction of signed orbits is compatible with toInt, so the flag of $a-b$ is a computable witness for the sign of $a.\mathrm{toInt}-b.\mathrm{toInt}$.
This module assembles the order surface (reflexivity, totality, trichotomy, sign-flag exclusivity) needed before reals and the forcing chain can treat integer comparisons as closed.
proof idea
Term-mode proof by three rewrites then omega. First apply nonnegFlag_eq_false_iff so the left side becomes $(\mathrm{sub},a,b).\mathrm{toInt}<0$. Rewrite the subtraction via sub_toInt to $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
Feeds the symmetric bridge lt_iff_nonnegFlag_sub_eq_false and sits in the display bundle for integer_order_certificate, whose doc states the internal signed-orbit order surface is closed. That certificate packages nonnegative and flag displays so later layers can treat integer comparison as a finished primitive rather than an open interface.
In the Recognition stack this is foundation plumbing under Arithmetic-from-Logic and the path toward Cauchy reals, not a forcing-chain landmark itself. Without a flag-to-order bridge, sign tests stay noncomputable relative to the structural Boolean layer. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.