negativeFlag_zero_sub
plain-language theorem explainer
The strict-negativity flag of zero minus a signed orbit equals that of the orbit's pointwise negation. Authors of the integer-order certificate cite this when equating subtraction-from-zero with structural negation. Proof is a one-line unfold of the negativity flag followed by rewrite through the matching nonnegativity identity.
Claim. For every signed orbit $a$, the strict-negativity flag of $0-a$ equals the strict-negativity flag of $-a$: $\mathrm{negFlag}(0-a)=\mathrm{negFlag}(-a)$.
background
Signed orbits are the internal integer model in Primitive Recognition Calculus: a pair (pos, neg) of distinction naturals, read as the formal difference pos - neg. Pointwise negation swaps the two components. The structural nonnegative flag decides whether an orbit represents a nonnegative integer; the negative flag is defined as its Boolean negation (strict negativity as failure of nonnegativity).
Internal order is defined by nonnegativity of differences: $a \le b$ when $b-a$ is nonnegative. Comparing zero against an orbit therefore reduces to the sign of $0-a$ and of $-a$. The sibling result nonnegFlag_zero_sub already equates the nonnegative flags of those two expressions; the present lemma is the dual statement for the negative flag.
proof idea
Term-mode, two steps. Unfold the definition of the negative flag (Boolean not of the nonnegative flag) on both sides. Rewrite with the already-proved identity that the nonnegative flag of $0-a$ equals the nonnegative flag of $-a$. The two Boolean negations then match, and the goal closes.
why it matters
Closes one of the sign-flag identities needed for the internal signed-orbit order surface. Downstream it is consumed by integer_order_certificate, whose doc-comment states that surface is closed and packages display lemmas for truncated subtraction, $\le$, absolute difference, and both signed nonnegativity and its flag form.
In the Recognition foundation this sits inside the integer layer that underwrites discrete counting before the forcing chain (T0–T8) and the Recognition Composition Law. It is bookkeeping rather than a landmark, but without the zero-subtraction duals the order certificate cannot assert that structural negation and subtraction-from-zero agree on sign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.