negativeFlag_sub_self
plain-language theorem explainer
For any signed orbit a, the self-difference a − a is not strictly negative: its negative flag is false. Order and certificate authors on the internal signed-orbit lattice cite this as the dual of the nonnegative self-difference law. The proof unfolds the flag definition and rewrites by the companion nonnegative result.
Claim. For every signed orbit $a$, the difference $a-a$ has negative flag equal to $\mathsf{false}$ (equivalently, $a-a$ is not strictly negative).
background
Signed orbits are the internal integer-like objects of the primitive recognition calculus: each is a pair of distinction naturals (pos, neg) with intended meaning pos − neg. Order on them is defined by nonnegativity of differences: a ≤ b when b − a is nonnegative.
Strict negativity is not a primitive field. The negative flag is defined as the Boolean negation of the structural nonnegative flag: negativeFlag z := !z.nonnegFlag. Thus any fact about one flag is dual to a fact about the other.
The companion lemma nonnegFlag_sub_self already records that (a − a).nonnegFlag = true, proved by reducing the difference to its integer image and using omega. The present statement is the dual Boolean claim needed for a closed order surface.
proof idea
Term-mode, three steps. Unfold negativeFlag to expose !·.nonnegFlag. Rewrite the inner nonnegative flag by nonnegFlag_sub_self a, which supplies true. Close with rfl, since !true = false. No separate arithmetic is needed; all integer content lives in the companion lemma.
why it matters
This is a small but required closure fact for the internal signed-orbit order. It feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed; that certificate packages display lemmas for truncated subtraction, ≤, absolute difference, and both signed-nonnegativity characterizations.
In the Recognition foundation stack this sits inside Primitive Recognition Calculus integer order, the discrete substrate on which later forcing and ladder constructions rest. It does not itself invoke T5–T8 or the Recognition Composition Law; it only guarantees that self-differences are never flagged strictly negative, matching the classical identity a − a = 0 ≥ 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.