negativeFlag_eq_false_iff_nonnegFlag_eq_true
plain-language theorem explainer
For any signed orbit difference, the negativity flag is false exactly when the nonnegativity flag is true. Anyone building the internal order on signed orbits cites this Boolean duality. The proof unfolds the definition of the negativity flag as Boolean negation and case-splits on the nonnegativity flag.
Claim. For every signed orbit $z$ (a pair of distinction naturals interpreted as $\mathrm{pos}-\mathrm{neg}$), the strict-negativity flag of $z$ equals $\mathsf{false}$ if and only if the structural nonnegativity flag of $z$ equals $\mathsf{true}$.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction naturals $(\mathrm{pos},\mathrm{neg})$ with intended meaning $\mathrm{pos}-\mathrm{neg}$. The structural nonnegativity flag is the Boolean comparison $\mathrm{leq}(\mathrm{neg},\mathrm{pos})$ on those sides. Strict negativity is defined purely as failure of that flag: the negativity flag is the Boolean negation of the nonnegativity flag.
The IntegerOrder module develops the internal order surface on these signed orbits (and later on ratio orbits). Order is defined by nonnegativity of differences, so the two flags must be complementary Boolean witnesses. This lemma records that complementarity as an iff.
proof idea
One short tactic proof. Unfold the definition of the negativity flag (Boolean not of the nonnegativity flag). Case-split on the Boolean value of the nonnegativity flag; both branches close by simplification. No external lemmas are required beyond the definitional unfolding.
why it matters
The lemma is the Boolean bridge used throughout IntegerOrder whenever a goal mentions one flag and the ambient hypothesis mentions the other. Downstream it is rewritten into the characterization of order by a non-negative difference (negativeFlag_sub_eq_false_iff_le), into sign-sensitive identities for reciprocal numerators, and into the balanced-negate absolute-value criterion. It also sits under the closed integer-order certificate that packages the signed nonnegativity displays. Within Recognition Science this is foundation scaffolding for the discrete order that later supports the forcing chain's integer and rational layers, not a physics identity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.