nonnegFlag_eq_false_iff
plain-language theorem explainer
The structural nonnegativity flag on a signed orbit difference is false exactly when the orbit's integer display is strictly negative. Order and comparison lemmas in the primitive recognition calculus cite this bridge between the Bool flag and the verifier integer. The proof is a short Boolean dual of the nonnegative case, finished by linear integer arithmetic.
Claim. For every signed orbit $z$ (a pair of distinction naturals with intended meaning $\mathrm{pos}-\mathrm{neg}$), the structural nonnegativity flag of $z$ equals $\mathsf{false}$ if and only if the integer display of $z$ satisfies $z_{\mathbb{Z}} < 0$.
background
In the primitive recognition calculus, integers arise as signed orbit differences. A signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals with intended meaning $\mathrm{pos}-\mathrm{neg}$ (K4.6). Its verifier display is the ordinary integer $\mathrm{toInt}(z)=\mathrm{pos.toNat}-\mathrm{neg.toNat}$.
The computable nonnegativity flag is defined by structural comparison: the flag is true precisely when $\mathrm{neg}\le\mathrm{pos}$ in the distinction-natural order. The companion theorem already equates the true flag with $0\le\mathrm{toInt}(z)$. This module reconstructs integer arithmetic from recognition orbits and feeds the later order infrastructure.
Upstream recovery maps from logic integers to $\mathbb{Z}$ supply the same display convention used here for signed orbits.
proof idea
Rewrite the goal via Boolean negation: flag equals false is equivalent to flag not equal to true. Apply the already-proved equivalence that the flag is true iff $0\le\mathrm{toInt}(z)$. The remaining biconditional is $\neg(0\le\mathrm{toInt}(z))\leftrightarrow\mathrm{toInt}(z)<0$, which both directions discharge by omega on integers. No case split on the orbit components is needed beyond what the true-case lemma already unfolded.
why it matters
This is the strict-negativity half of the flag–display agreement used throughout the integer-order layer. Downstream results include comparison characterizations (when the structural comparator returns greater-than), preservation of the flag under scaling by a nonzero distinction natural and under balanced pairs, the false flag on the negation of a nonzero orbit, and the subtraction criterion that identifies $a<b$ with a false flag on $a-b$.
Together with the true-case sibling, it closes the bridge between structural Bool flags and the integer order forced from recognition orbits. That bridge is load-bearing for later arithmetic built on signed differences in the foundation stack that recovers integers from logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.