nonnegFlag_zero_sub
plain-language theorem explainer
The structural nonnegative flag of zero minus a signed orbit equals the flag of that orbit's pointwise negation. Order and sign lemmas on signed orbits cite this to move between subtraction from zero and negation. The proof cases on the flag, rewrites both sides through the integer recovery map, and closes with omega.
Claim. For every signed orbit $a$, the structural nonnegative flag of $0-a$ equals the structural nonnegative flag of $-a$.
background
Signed orbits are the internal integer carriers in the primitive recognition calculus: each value is a pair of distinction-natural sides (pos, neg). The recovery map toInt sends a signed orbit to an ordinary integer by subtracting the two sides as naturals. Pointwise negation swaps the two sides, and is known to satisfy $(\mathrm{negate}, a).\mathrm{toInt} = -a.\mathrm{toInt}$.
The nonnegative flag is a computable Bool obtained by structural comparison of the two sides (DistinctionNat.leq of neg against pos). Upstream characterizations pin it to the recovered integer: the flag is true iff $0 \le z.\mathrm{toInt}$, and false iff $z.\mathrm{toInt} < 0$. Subtraction of signed orbits is likewise compatible with toInt.
This module builds the order surface on those carriers. The present identity is the flag-level form of $0-a = -a$ under the structural nonnegative test.
proof idea
Case on the Bool value of the nonnegative flag of $\mathrm{negate}, a$.
If the flag is false, rewrite the goal with the false-characterization, expand subtraction and zero under toInt, obtain $(\mathrm{negate}, a).\mathrm{toInt} < 0$ from the case hypothesis, push negation through toInt to get $-a.\mathrm{toInt} < 0$, and finish by omega on the integer inequality for $(0-a).\mathrm{toInt}$.
If the flag is true, the same pattern uses the true-characterization: $0 \le (\mathrm{negate}, a).\mathrm{toInt}$, rewrite via negate_toInt, and omega again. No separate algebraic identity for subtraction of zero is needed beyond the toInt bridge lemmas.
why it matters
This is a small but load-bearing bridge in the signed-orbit order layer. Downstream, negativeFlag_zero_sub is a one-line unfold-and-rewrite of the negative flag through this identity, so sign-flip lemmas inherit the same zero-subtraction coherence.
It also sits under integer_order_certificate, whose doc states that "the internal signed-orbit order surface is closed." That certificate packages the display lemmas for truncated subtraction, structural leq, absolute difference, and the nonnegative flag characterizations. Closing flag behavior under $0-a$ versus negation keeps the certificate's signed-nonneg displays consistent with ordinary integer arithmetic.
In the broader Recognition foundation, integers are recovered from logic rather than postulated; flag-level identities like this ensure the order surface matches the recovered Int order without smuggling classical sign conventions into the structural layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.