nonnegFlag_negate_ofOrbit_of_ne_zero
plain-language theorem explainer
For nonzero distinction-natural n, embedding n as a signed orbit and then negating yields a strictly negative signed orbit (nonnegFlag false). Order and reciprocal lemmas cite this when they need the sign of −n for n>0. The proof rewrites the flag to an integer inequality via toInt, reduces ofOrbit and negate, and closes with omega after injectivity of toNat.
Claim. Let $n$ be a distinction-natural with $n \neq 0$. Form the signed orbit of $n$ (the nonnegative embedding) and negate it by swapping positive and negative limbs. Then the nonnegativity flag of that negated orbit equals false; equivalently its integer value is strictly negative.
background
In the primitive recognition calculus, integers are represented as signed orbits: a pair of distinction-naturals (pos, neg) whose integer reading is $\mathrm{toInt} = \mathrm{toNat}(\mathrm{pos}) - \mathrm{toNat}(\mathrm{neg})$. The map $\mathrm{ofOrbit}$ embeds a distinction-natural $n$ as the nonnegative signed orbit with that positive limb and zero negative limb. Negation swaps the two limbs, and $\mathrm{negate_toInt}$ records $(\mathrm{negate}, a).\mathrm{toInt} = -a.\mathrm{toInt}$.
The Boolean $\mathrm{nonnegFlag}$ is the display surface for the order: it is false precisely when $\mathrm{toInt} < 0$ (via $\mathrm{nonnegFlag_eq_false_iff}$). Distinction-naturals carry a $\mathrm{toNat}$ reading into ordinary $\mathbb{N}$, with $\mathrm{toNat}(0)=0$ and injectivity of $\mathrm{toNat}$.
This module builds the internal order on those signed orbits (reflexivity, totality, trichotomy, sign-flag exclusivity) so that later certificates can treat integer comparison as a closed surface rather than an external axiom.
proof idea
Rewrite the goal with three identities: $\mathrm{nonnegFlag}=\mathrm{false}$ iff $\mathrm{toInt}<0$; $\mathrm{toInt}$ of a negation is the ordinary integer negation; and $\mathrm{toInt}$ of $\mathrm{ofOrbit},n$ is $\mathrm{toNat}(n)$ as an integer. The goal becomes $-(\mathrm{toNat},n)<0$, i.e. $\mathrm{toNat},n\neq 0$.
If $\mathrm{toNat},n=0$, injectivity of $\mathrm{toNat}$ plus $\mathrm{toNat_zero}$ forces $n=0$, contradicting the hypothesis. With $\mathrm{toNat},n\neq 0$ in hand, omega finishes the integer inequality.
why it matters
This is a small but load-bearing sign lemma in the integer-order layer of the recognition calculus. Downstream, $\mathrm{recipNonzero_num_nonnegFlag_eq}$ uses it when tracking how reciprocal numerators inherit (or flip) nonnegativity flags under nonzero hypotheses. It also sits under $\mathrm{integer_order_certificate}$, whose doc-comment states that "the internal signed-orbit order surface is closed" and packages nonnegFlag display laws among the certificate fields.
In the broader Recognition Science stack, closed internal arithmetic and order are prerequisites for later forcing and mass-ladder constructions; they keep comparison and sign reasoning inside the primitive orbit language rather than smuggling classical $\mathbb{Z}$ axioms. The result is fully proved (no sorry), so it is available as a stable building block for those certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.