nonnegFlag_sub_self
plain-language theorem explainer
Self-subtraction of any signed orbit difference is flagged nonnegative. Order-theory and certificate authors cite it to lock reflexivity of the internal integer order at zero. The proof rewrites the flag to an integer inequality via the structural nonnegative characterization and the subtraction-to-integer law, then closes with omega.
Claim. For every signed orbit difference $a$, the self-difference $a-a$ has nonnegative flag equal to true. Equivalently, writing $\mathrm{toInt}$ for the integer value of a signed orbit, $0 \le (a-a).\mathrm{toInt}$.
background
Signed orbits are the primitive integer carriers in the Recognition calculus: a pair of distinction naturals (pos, neg) with intended meaning pos - neg. Their computable nonnegative flag is the structural comparison leq neg pos; it is designed so that the flag is true exactly when the integer value is nonnegative.
The companion lemma nonnegFlag_eq_true_iff states that equivalence explicitly: z.nonnegFlag = true ↔ 0 ≤ z.toInt. Subtraction of signed orbits is defined so that it respects integer values: (sub a b).toInt = a.toInt - b.toInt. Together these give a bridge from a purely structural Boolean flag to ordinary integer arithmetic.
This module builds the internal order surface on those carriers (reflexivity, totality, trichotomy, sign-flag exclusivity). The present fact is the zero case of reflexivity for the nonnegative flag under self-subtraction.
proof idea
Term-style rewrite proof. First apply the characterization that the nonnegative flag is true iff the integer value is nonnegative. Then rewrite the integer value of sub a a by the subtraction law, obtaining the goal 0 ≤ a.toInt - a.toInt. Close with omega, which discharges the trivial integer identity.
why it matters
Feeds the sibling negativeFlag_sub_self, which unfolds the negative flag as failure of the nonnegative flag and rewrites with this lemma to conclude the negative flag of a-a is false. Both facts support the closed order surface packaged by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed" and lists the signed nonnegative flag display among its fields.
In the broader Recognition foundation this is bookkeeping on the integer layer beneath the forcing chain (T0–T8): before J-cost uniqueness, phi, the eight-tick octave, or D=3 can be stated cleanly, the signed-orbit carriers must behave like ordinary integers under order and sign. Reflexivity of nonnegativity at zero is the minimal sanity check that the structural flag matches the intended integer meaning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.