negativeFlag_sub_zero
plain-language theorem explainer
Subtracting the zero signed orbit leaves the negativity flag unchanged. Order and certificate lemmas for the internal signed-orbit integers cite this identity. The proof unfolds negativity as the Boolean negation of the nonnegative flag and rewrites with the matching nonnegativity-under-subtraction-of-zero lemma.
Claim. For every signed orbit $a$, the strict-negativity flag of $a-0$ equals the strict-negativity flag of $a$: $\mathrm{neg}(a-0)=\mathrm{neg}(a)$.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction naturals interpreted as a difference $\mathrm{pos}-\mathrm{neg}$. The structural nonnegative flag on a signed orbit is the Boolean that records whether that difference is nonnegative in the internal integer model; the strict-negativity flag is defined simply as its Boolean negation.
The local module builds the order surface on these signed orbits: $a\le b$ means $b-a$ is nonnegative. Subtracting the zero orbit is the identity on the underlying integer value, so every sign-sensitive Boolean attached to $a-0$ must match the same Boolean on $a$. The sibling result that subtraction of zero preserves the nonnegative flag is the direct upstream input.
proof idea
One short tactic proof. Unfold the definition of the negativity flag (Boolean not of the nonnegative flag). Rewrite with the already-proved fact that $(a-0)$ has the same nonnegative flag as $a$. Equality of the negated Booleans is then immediate.
why it matters
This is a small but necessary identity in the closed order package for signed orbits. It is consumed by the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed and which packages display lemmas for truncated subtraction, $\le$, absolute difference, and both the Prop-level and flag-level nonnegativity characterizations.
Within Recognition Science foundation work, the signed-orbit integers sit under the primitive recognition calculus that supports later forcing and cost structure. The lemma does not itself touch J-uniqueness, $\varphi$, or the eight-tick octave; it only keeps the integer-order certificate honest so those layers can treat signed differences as an ordered ring-like surface without flag drift at zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.