nonnegFlag
plain-language theorem explainer
A signed orbit difference is flagged nonnegative exactly when its negative side is structurally at most its positive side under the Boolean order on finite distinction orbits. Anyone building the choice-free order, absolute value, or multiplication-monotonicity lemmas on signed orbits cites this flag as the computable witness. The body is a one-line structural comparison; no arithmetic on integers is involved.
Claim. Let $z=(p,n)$ be a signed orbit difference (intended meaning $p-n$), with $p,n$ finite distinction-orbit positions. The nonnegative flag of $z$ is the Boolean value of the structural comparison $n\le p$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, used wherever a natural count of distinctions is needed without committing to a numeral base.
A signed orbit packages two such positions as a formal difference $p-n$. The Boolean order leq on distinction orbits is defined by structural recursion alone: zero is below everything, successor is never below zero, and successors compare by peeling. That order is the only comparison primitive used here.
The surrounding module builds integers and rationals from these orbit objects, keeping every predicate computable and free of classical choice on $\mathbb{Z}$.
proof idea
Pure definition: apply the structural Boolean order on distinction orbits to the pair $(z.n, z.p)$. No lemmas, no tactics, no coercion through $\mathbb{Z}$.
why it matters
This flag is the structural stand-in for "$z\ge 0$" throughout the choice-free signed-orbit order. Downstream it appears in the equivalence of order with a nonnegative difference, the characterization of $0\le z$, preservation of the flag under right-multiplication by a nonzero orbit, and absolute-value identities that recover toInt on the nonnegative cone. Those lemmas explicitly replace earlier routes that went through $\mathbb{Z}$ and were marked choice-tainted; the ratio rungs in the grow layer depend on the choice-free versions. In the broader Recognition stack this sits under the integers-from-logic layer that feeds the forcing chain's discrete arithmetic, not yet at T5--T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.