nonnegFlag_ofOrbit
plain-language theorem explainer
Any δ-orbit position, embedded as a signed orbit with zero negative part, is flagged nonnegative. Order and sign lemmas for the internal integer surface cite this fact. The proof rewrites the flag through the integer interpretation and applies nonnegativity of natural casts.
Claim. For every distinction-natural $n$, the signed orbit obtained by placing $n$ in the positive slot and zero in the negative slot has nonnegative flag equal to $\mathsf{true}$. Equivalently, its integer value satisfies $0 \le n$ under the standard embedding $\mathbb{N}\hookrightarrow\mathbb{Z}$.
background
In the primitive recognition calculus, integers are realized as signed orbit differences: a structure with two distinction-natural sides, read as $\mathrm{pos}-\mathrm{neg}$. The map that sends a bare δ-orbit position $n$ to the pair $\langle n,0\rangle$ is the canonical nonnegative embedding.
The nonnegative flag is a computable Boolean obtained by structural comparison of the two sides (negative side $\le$ positive side). It is proved equivalent to the usual inequality $0\le z$ after interpreting the signed orbit as an ordinary integer.
Distinction naturals themselves come from the logic-to-arithmetic bridge: their toNat map reads off the iteration count of the step constructor, so the embedded orbit evaluates exactly to that natural number in $\mathbb{Z}$.
proof idea
Term-mode rewrite chain. First apply the characterization that the nonnegative flag is true if and only if the integer value is nonnegative. Then simplify the integer value of the canonical embedding to the natural cast of $n$. Finish with the standard fact that every natural number is nonnegative in $\mathbb{Z}$.
why it matters
This is a basic positivity lemma on the signed-orbit integer surface. It feeds the companion statement that the same embedding has negative flag false, and it appears in the reciprocal-nonzero numerator identity that preserves the nonnegative flag under inversion of nonzero ratios.
Downstream it supports the integer-order certificate, which packages display lemmas closing the internal order surface (signed nonnegativity flag equivalent to $0\le\mathrm{toInt}$, truncated subtraction, absolute difference, and so on). Within Recognition Science foundation work this is scaffolding for ordered arithmetic built from recognition orbits rather than postulated $\mathbb{Z}$, prior to the forcing chain (T5–T8) that extracts $J$, $\varphi$, the eight-tick period, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.