nonneg_iff_toInt_nonneg
plain-language theorem explainer
Internal nonnegativity of a signed orbit (balancing against a pure positive orbit) is equivalent to its integer display being nonnegative. Order certificates, the signed order relation, the structural nonneg flag, and the rational positivity bridge all cite this equivalence. The proof is a two-sided constructor: reduce via the balanced-to-integer display lemma and finish with omega on Nat/Int arithmetic.
Claim. For every signed orbit $z$ (a pair of distinction-natural counts read as $\mathrm{pos}-\mathrm{neg}$), $z$ is internally nonnegative if and only if $0\le\mathrm{toInt}(z)$. Internal nonnegativity means there exists a distinction-natural $k$ such that $z$ balances with the pure positive orbit $\langle k,0\rangle$.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction-naturals $(\mathrm{pos},\mathrm{neg})$, intended as the difference $\mathrm{pos}-\mathrm{neg}$. The verifier map $\mathrm{toInt}$ sends that pair to an ordinary integer. A pure positive orbit is $\mathrm{ofOrbit}(n)=\langle n,0\rangle$, and $\mathrm{ofOrbit}(n).\mathrm{toInt}=n.\mathrm{toNat}$.
Internal nonnegativity is the existence statement: $z$ balances with some pure positive orbit. Balance is the internal PRC equivalence on signed orbits; the upstream lemma K4.9 states that balance agrees with equality of integer displays, giving the bridge from the internal relation to the conservative $\mathbb{Z}$ view.
The local module builds integer and rational structure from orbit arithmetic without classical choice in the display lemmas. This theorem is the nonnegativity half of that display bridge.
proof idea
Split the biconditional with constructor.
Forward: from a witness $k$ and a balance hypothesis, apply balanced_iff_toInt_eq against ofOrbit k, rewrite with ofOrbit_toInt, and close by omega (the display is a nonnegative natural).
Backward: from $0\le z.\mathrm{toInt}$, take the witness DistinctionNat.ofNat z.toInt.toNat. Rewrite the balance goal by balanced_iff_toInt_eq, ofOrbit_toInt, and toNat_ofNat, then finish with omega.
No induction; pure display transport plus linear arithmetic.
why it matters
This is the nonnegativity display bridge for signed orbits in the foundation layer. Downstream, le_iff_toInt_le unfolds order as nonnegativity of a difference and rewrites through this lemma; nonnegFlag_eq_true_iff_nonneg ties the structural flag to the same Prop; nonneg_iff_of_balanced transports nonnegativity across balance by rewriting both sides here.
It is also a field of the integer-order certificate (signed_nonneg_display), which records that the internal signed-orbit order surface is closed. The rational-field lemma positive_iff_toRat_pos sits on the same display pattern for ratios.
In Recognition Science terms this is pre-physics scaffolding: integers and their order are recovered from distinction orbits before the forcing chain (T5 J-cost, T6 $\varphi$, T7 eight-tick, T8 $D=3$) is applied. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.