negativeFlag_sub_eq_false_iff_le
plain-language theorem explainer
For signed orbits a and b, the difference a−b fails the negative flag exactly when b≤a. Order and certificate lemmas in the primitive recognition calculus cite this bridge between the Boolean negativity flag and the internal order. The proof is a two-step rewrite through the nonnegativity flag and the existing nonneg-sub characterization of ≤.
Claim. For signed orbits $a,b$, the Boolean negative flag of $a-b$ equals false if and only if $b\le a$ in the internal signed-orbit order (equivalently: $a-b$ is nonnegative).
background
Signed orbits are the K4.6 integer layer: pairs (pos, neg) of distinction naturals, read as the formal difference pos − neg. The structure carries a Boolean nonnegFlag and defines negativeFlag as its negation, so negativity is literally failure of structural nonnegativity.
Internal order is defined by nonnegativity of a difference: a ≤ b means b − a is nonnegative. Upstream, nonnegFlag_sub_iff_le already equates (a − b).nonnegFlag = true with b ≤ a, via the integer embedding and omega. A companion lemma equates negativeFlag = false with nonnegFlag = true by unfolding the Boolean negation.
This module builds the order surface on that signed-orbit arithmetic so later certificates can treat ≤, flags, and truncated displays as a closed package.
proof idea
Term-mode proof by two rewrites. First apply negativeFlag_eq_false_iff_nonnegFlag_eq_true to replace (a−b).negativeFlag = false by (a−b).nonnegFlag = true. Then apply nonnegFlag_sub_iff_le, which already equates that nonnegativity flag on the difference with SignedOrbit.le b a. No case split or arithmetic remains at this layer.
why it matters
Closes the negative-flag side of the order dictionary for signed orbits. Downstream, le_iff_negativeFlag_sub_eq_false is the swapped form obtained by symmetry, and both feed the integer-order surface that integer_order_certificate packages ("the internal signed-orbit order surface is closed"). That certificate is part of the foundation stack that reconstructs arithmetic and order from recognition primitives before the forcing chain (T0–T8) and physical constants are attached. Without this bridge, Boolean sign flags and the Prop-level order would remain separate interfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.