nonneg
plain-language theorem explainer
Internal nonnegativity for signed orbits: z is nonnegative when it balances against some pure positive orbit. Cost-algebra and distinction-to-cost developments cite this predicate as the structural stand-in for z ≥ 0 before real embedding. The body is a one-line existential over the internal PRC balance relation.
Claim. A signed orbit $z=(p,n)$ (intended meaning $p-n$) is nonnegative when there exists a distinction-orbit length $k$ such that $z$ balances with the pure positive orbit $(k,0)$: equivalently $p+0=k+n$, i.e. $p=k+n$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A SignedOrbit is a pair of such orbits, read as a signed difference $p-n$.
Two signed orbits are balanced when their lengths satisfy the cross-equality $a.p+b.n=b.p+a.n$; that is the internal integer relation of the module, defined entirely on $\delta$-orbit positions. The constructor ofOrbit k builds the pure nonnegative representative $(k,0)$.
The local setting is the IntegerRational layer of PRC: integers are recovered as balance-classes of signed orbits before any real or rational embedding. Nonnegativity is therefore stated internally, without reference to $\mathbb{Z}$ or $\mathbb{R}$.
proof idea
Pure definition, not a proved theorem. The predicate expands to the existential $\exists k,,\mathrm{balanced}(z,\mathrm{ofOrbit},k)$. Unfolding balance and ofOrbit yields the concrete length equation $z.p=k+z.n$. No tactics or upstream lemmas are applied.
why it matters
This predicate is the structural nonnegativity gate used across the foundation-to-algebra bridge. Downstream, CostAlgebraData packages a cost with a nonneg field, and canonicalCostAlgebra fills it with $J$-nonnegativity; the present definition supplies the orbit-level meaning of that field before $J$ is introduced. CostFunction in CostFromDistinction likewise requires $0\le C\Gamma$ for every configuration, and cost_pos_iff_inconsistent turns nonnegativity plus dichotomy into the inconsistency test.
It also appears in gap-weight projection (w8_projected_nonneg) and in golden-integer trichotomy on the delta spine. In the forcing chain it sits under the cost side of T5 (unique $J$) and the Recognition Composition Law: without an internal nonnegativity notion, the cost algebra cannot be stated on PRC carriers alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.