nonnegFlag_eq_true_iff
plain-language theorem explainer
The structural nonnegative flag on a signed orbit equals true exactly when its integer display is nonnegative. Absolute-value, balance, comparison, and the integer-order certificate all cite this bridge. The proof unfolds both sides, rewrites through the Boolean-to-Nat order lemma, and closes both directions by omega.
Claim. Let $z=(p,n)$ be a signed orbit (intended meaning $p-n$). The structural flag $\mathrm{leq}(n,p)$ equals true if and only if $0\le \mathrm{toInt}(z)$, where $\mathrm{toInt}(z)=p^{\mathbb{N}}-n^{\mathbb{N}}$ in $\mathbb{Z}$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero/successor). A SignedOrbit is a pair of such orbits $(p,n)$, documented as the signed difference $p-n$ (K4.6).
The verifier display toInt sends $z$ to $(p.\mathrm{toNat}:\mathbb{Z})-(n.\mathrm{toNat}:\mathbb{Z})$. Independently, nonnegFlag is the computable Boolean obtained by structural comparison: $\mathrm{leq},n,p$. Upstream, leq_eq_true_iff already equates that Boolean to the ordinary Nat order on the recovered naturals, with a choice-free induction proof (axiom footprint [propext]).
This lemma is the signed lift of that display agreement: the flag is true precisely when the integer display is nonnegative.
proof idea
Term-mode proof. Unfold nonnegFlag and SignedOrbit.toInt, so the goal becomes $\mathrm{leq},n,p=\mathrm{true}\leftrightarrow 0\le p^{\mathbb{N}}-n^{\mathbb{N}}$. Rewrite the left side by DistinctionNat.leq_eq_true_iff to $n^{\mathbb{N}}\le p^{\mathbb{N}}$. Split the biconditional; each direction is pure integer arithmetic closed by omega.
why it matters
This is the signed nonnegative display bridge recorded in integer_order_certificate as signed_nonneg_flag_display. Downstream order infrastructure depends on it heavily: abs_toInt_of_nonnegFlag recovers absolute value from the flag; balanced_ofOrbit_abs_iff_nonnegFlag and its negate twin equate balance with the flag; comparison lemmas (cmp_eq_lt_iff, cmp_eq_lt_of_lt) and multiplicative order facts under a nonnegative flag all route through it.
In the Recognition foundation stack this closes the Boolean/structural side of integer order against the verifier $\mathbb{Z}$ display, so later forcing and arithmetic layers can treat nonnegativity as a computable flag without leaving the orbit calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.