negativeFlag
plain-language theorem explainer
Boolean flag marking a signed orbit difference as strictly negative: true exactly when the structural nonnegative flag fails. Integer-order lemmas cite it for sign-sensitive comparison, absolute value, and balanced canonical forms. The body is a one-line Boolean negation of the nonnegative flag.
Claim. For a signed orbit $z=(p,n)$ (intended value $p-n$), define the negative flag by $\mathrm{neg}(z) := \neg\,\mathrm{nonneg}(z)$, where $\mathrm{nonneg}(z)$ holds exactly when $n\le p$ under the structural order on distinction naturals. Thus the flag is true precisely when that order comparison fails.
background
In the primitive recognition calculus, integers are not taken as primitives. A SignedOrbit is a pair of distinction naturals $(p,n)$ with intended meaning $p-n$. Display as an ordinary integer is a derived verifier map, not the carrier itself.
Nonnegativity is decided structurally: the nonnegative flag is the Boolean outcome of the distinction-natural order test $n\le p$. That test is computable and does not pass through $\mathbb{Z}$. The present definition simply dualizes that flag.
The surrounding module builds truncated subtraction, absolute difference, and the signed-orbit arithmetic needed before an ordered ring certificate can be stated. Negativity is the complementary Boolean used by those order lemmas.
proof idea
Definitional one-liner: return the Boolean negation of the structural nonnegative flag on the same signed orbit. No lemmas are applied; the meaning is entirely by dualization of the upstream nonnegative flag (itself DistinctionNat.leq of the negative side against the positive side).
why it matters
This flag is the sign gate for the IntegerOrder layer. Downstream results use it to recover absolute value on negative carriers (abs_toInt_of_negativeFlag), to place a negative orbit in balanced negated-absolute form (balanced_of_negativeFlag, balanced_sign_canonical), and to reverse comparison under left or right multiplication by a negative factor (cmp_mul_left_of_negativeFlag, cmp_mul_right_of_negativeFlag). It also appears in the order certificate and in characterizations of $\le$ via the flag on a difference.
Within Recognition Science foundation work, signed orbits are the pre-arithmetic substrate before continuum or physical constants appear. Getting a clean, structural negative test is a prerequisite for ordered arithmetic on that substrate; the flag is cited heavily (dozens of use sites) precisely because later comparison and balancing theorems branch on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.