nonnegFlag_eq_true_iff_nonneg
plain-language theorem explainer
The structural Boolean flag on a signed orbit is true exactly when that orbit is internally nonnegative. Anyone bridging the computable comparison layer to the Prop-level nonnegativity predicate in the integer-rational calculus would cite this. The proof is a one-line rewrite chaining the flag-to-integer and nonnegativity-to-integer equivalences.
Claim. For every signed orbit $z$ (a pair of distinction-naturals read as $\mathrm{pos}-\mathrm{neg}$), the structural nonnegative flag of $z$ equals true if and only if $z$ is internally nonnegative: there exists a positive orbit against which $z$ balances.
background
A signed orbit is the K4.6 difference type: a pair $(\mathrm{pos},\mathrm{neg})$ of distinction-naturals, intended as $\mathrm{pos}-\mathrm{neg}$. It carries a verifier integer display $\mathrm{toInt}$, and a balanced relation that equates two signed orbits when their displays agree.
Internal nonnegativity is the Prop that $z$ balances against some pure positive orbit (an orbit with zero negative part). Separately, the structural nonnegative flag is the Boolean obtained by comparing the two sides with the distinction-natural order: $\mathrm{leq},z.\mathrm{neg},z.\mathrm{pos}$.
Two prior results already pin both notions to the same integer inequality $0\le z.\mathrm{toInt}$: the flag is true exactly when the display is nonnegative, and internal nonnegativity holds exactly when the display is nonnegative. This theorem closes the triangle.
proof idea
One-line wrapper. Rewrite with the two intermediate equivalences: structural flag true iff $0\le z.\mathrm{toInt}$, and internal nonnegativity iff $0\le z.\mathrm{toInt}$. Transitivity of $\leftrightarrow$ yields the claim. No new case analysis.
why it matters
In the primitive recognition calculus, signed orbits are the integer layer under the rational and growth constructions. Keeping a computable Boolean flag aligned with the internal Prop is what lets later order lemmas stay executable while still talking about genuine nonnegativity.
The sole recorded consumer is the choice-free restatement of the structural Boolean order against the $\mathbb{N}$ order in the signed-orbit growth module: that development deliberately avoids classical $\mathrm{Bool}$/$\mathrm{Decidable}$ simp paths that pull $\mathrm{Classical.choice}$, and needs flag-to-Prop bridges of this shape to stay inside ${\mathrm{propext},\mathrm{Quot.sound}}$.
Within the broader Recognition forcing chain this sits in foundation scaffolding (orbit arithmetic), not yet at T5–T8; it is bookkeeping that keeps the integer display honest before cost and dimension forcing are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.