negativeFlag_ofOrbit
plain-language theorem explainer
Any signed orbit built from a plain distinction count (pos = n, neg = 0) is not strictly negative: its negative flag is false. Order and ratio lemmas that need the sign of ofOrbit cite this. The proof is a short rewrite from the matching nonnegativity flag lemma plus the definition of negativeFlag as Boolean negation of nonnegFlag.
Claim. For every distinction count $n$, the signed orbit $\mathrm{ofOrbit}(n) = \langle n, 0\rangle$ satisfies $\mathrm{negativeFlag}(\mathrm{ofOrbit}(n)) = \mathsf{false}$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A SignedOrbit is a pair (pos, neg) of such counts, read as the difference pos − neg (K4.6).
ofOrbit n embeds a bare count as the nonnegative signed orbit ⟨n, 0⟩. The structural nonnegative flag on a signed orbit is the Boolean that records whether that difference is nonnegative in the internal integer model; negativeFlag is defined as its Boolean negation (“strict negativity as failure of the structural nonnegative flag”).
The sibling lemma nonnegFlag_ofOrbit already shows that ofOrbit n has nonnegative flag true, via the bridge nonnegFlag_eq_true_iff and ofOrbit_toInt together with nonnegativity of the natural cast.
proof idea
Obtain hnonneg : (ofOrbit n).nonnegFlag = true from nonnegFlag_ofOrbit. Unfold negativeFlag to !nonnegFlag, rewrite with hnonneg, and close by rfl (!true = false). Pure definitional reduction off the nonnegative companion.
why it matters
Closes the negative half of the sign story for the canonical nonnegative embedding of distinction counts. Downstream, recipNonzero_num_negativeFlag_eq uses it when tracking how reciprocal of a nonzero ratio acts on the numerator’s negative flag (via negate-ofOrbit cases). It also sits under the closed integer-order surface: integer_order_certificate packages the signed nonnegative displays that this flag pair supports.
In the Recognition foundation stack this is bookkeeping for the internal Z-order before rationals and the phi-ladder mass formula; it is not itself a forcing step (T5–T8), but it keeps signed-orbit order decidable and consistent with the nonnegative cone used later for comparison and reciprocity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.