nonnegFlag_sub_zero
plain-language theorem explainer
Subtracting the zero signed orbit leaves the structural nonnegativity flag unchanged. Order and certificate lemmas cite this when reducing comparisons against zero to the bare flag on a. The proof cases on the Boolean flag, rewrites through the toInt characterizations and subtraction identity, then closes both branches by omega on the integer inequality.
Claim. For every signed orbit $a$ (pair of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$), the structural nonnegativity flag of $a-0$ equals the nonnegativity flag of $a$.
background
Signed orbits are the internal integer model in the primitive recognition calculus: a structure with two DistinctionNat sides, intended as $\mathrm{pos}-\mathrm{neg}$. The recovery map toInt sends a signed orbit to an ordinary Int. Subtraction on signed orbits is defined so that it intertwines with ordinary subtraction: $(a-b).\mathrm{toInt}=a.\mathrm{toInt}-b.\mathrm{toInt}$, and zero maps to $0$.
The nonnegativity flag is a Boolean computed by structural comparison of the two sides (leq of the negative side against the positive side). It is characterized by the integer picture: the flag is true iff $0\le a.\mathrm{toInt}$, and false iff $a.\mathrm{toInt}<0$. The IntegerOrder module builds the order surface and certificate on top of these flags and the underlying distinction-nat displays.
proof idea
Case-split on the Boolean value of $a$'s nonnegativity flag.
False branch: rewrite the goal with the false-characterization and the identities $(a-0).\mathrm{toInt}=a.\mathrm{toInt}-0.\mathrm{toInt}$ and $0.\mathrm{toInt}=0$. The hypothesis gives $a.\mathrm{toInt}<0$, so omega yields $(a-0).\mathrm{toInt}<0$, hence the flag of $a-0$ is false.
True branch: same rewrites with the true-characterization; $0\le a.\mathrm{toInt}$ implies $0\le(a-0).\mathrm{toInt}$ by omega, so the flag stays true.
why it matters
This is a small but necessary stability fact for the signed-orbit order: comparisons against zero can be read off the bare flag without inserting an explicit zero subtraction. It is used immediately by the twin lemma that the negativity flag is likewise invariant under subtracting zero, and it feeds the closed integer-order certificate (integer_order_certificate), whose fields package the nonnegativity display and flag characterizations for the order surface.
In the Recognition foundation stack this sits under the integers-from-logic construction: once signed orbits recover ordinary integers, order and sign must be stable under the zero of that group so later forcing and calculus layers can treat nonnegativity as an intrinsic structural property rather than a presentation artifact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.