nonnegFlag_negate_ofOrbit_eq_true_iff_zero
plain-language theorem explainer
Negating a nonnegative signed orbit built from a distinction-natural n yields a nonnegative flag if and only if n is zero. Order and certificate authors cite this when closing the signed-orbit order surface: the only orbit whose opposite is still nonnegative is the zero orbit. The proof is a two-direction iff via the flag-to-integer bridge, negate/ofOrbit toInt lemmas, and a short omega/norm_num finish.
Claim. For every distinction-natural $n$, the structural nonnegative flag of the pointwise negation of the nonnegative signed orbit built from $n$ equals true if and only if $n$ is the zero distinction-natural.
background
In the primitive recognition calculus, integers are represented as signed orbits: pairs of distinction-naturals (pos, neg) with integer value toInt = pos.toNat - neg.toNat. The constructor ofOrbit n builds the nonnegative representative ⟨n, 0⟩. Pointwise negate swaps the two sides, so negate(ofOrbit n) is ⟨0, n⟩ and has toInt = -n.toNat.
The computable flag nonnegFlag is structural comparison leq neg pos; the bridge lemma states it equals true exactly when 0 ≤ toInt. Together these give a pure Boolean test for nonnegativity without leaving the orbit surface.
The local module develops the order theory of these signed orbits (reflexivity, totality, trichotomy, sign-flag exclusivity). Upstream arithmetic supplies toNat_zero : toNat zero = 0 and injectivity of toNat, which pin the zero case.
proof idea
Term-mode constructor on the biconditional.
Forward: assume the flag is true. Rewrite by nonnegFlag_eq_true_iff, negate_toInt, and ofOrbit_toInt to obtain 0 ≤ -n.toNat. Apply toNat injectivity, reduce the goal to toNat n = 0 via toNat_zero, and close with omega.
Backward: substitute n = zero, rewrite by the same three lemmas plus toNat_zero, and finish with norm_num (the inequality 0 ≤ 0 holds).
why it matters
Feeds the single downstream parent integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, leq, absolute difference, and the signed nonnegative flag bridge; this theorem is the zero-specialization needed so that negation interacts cleanly with the nonnegative cone.
In the Recognition foundation stack, signed orbits are the integer layer beneath the rational and cost calculus that eventually force the J-cost and the T0–T8 chain. Closing order facts at this layer keeps the arithmetic surface free of external Int axioms beyond the displayed bridges. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.