zero_le_iff_nonnegFlag
plain-language theorem explainer
For any signed orbit z, the order relation 0 ≤ z holds exactly when the structural nonnegative flag of z is true. Order and arithmetic developers cite this to move between the Prop-level order and the Bool flag used in certificates and reciprocal lemmas. The proof is a three-rewrite chain through the toInt bridge and the flag characterization.
Claim. For every signed orbit $z$ (pair of distinction naturals interpreted as $\mathrm{pos}-\mathrm{neg}$), one has $0 \le z$ if and only if the computable nonnegative flag of $z$ equals $\mathsf{true}$.
background
Signed orbits are the internal integer model in the primitive recognition calculus: a structure with fields pos and neg (distinction naturals), intended as the difference $\mathrm{pos}-\mathrm{neg}$. The internal order is defined by nonnegativity of the difference: $a \le b$ means $b-a$ is nonnegative.
The nonnegative flag is the computable Bool obtained by structural comparison of the two sides (DistinctionNat.leq of neg against pos). Upstream, le_iff_toInt_le identifies the internal order with ordinary integer order on the toInt embedding, and nonnegFlag_eq_true_iff says the flag is true exactly when $0 \le z.\mathrm{toInt}$. The zero orbit maps to integer zero under toInt.
This module develops the order surface on signed orbits (reflexivity, totality, trichotomy, sign-flag exclusivity) needed before rationals and certificates.
proof idea
Term-mode proof by three rewrites. First apply le_iff_toInt_le to replace $0 \le z$ by $0.\mathrm{toInt} \le z.\mathrm{toInt}$. Then rewrite zero_toInt so the left side is ordinary $0$. Finally apply nonnegFlag_eq_true_iff, which equates the flag being true with $0 \le z.\mathrm{toInt}$. The three characterizations collapse to the stated biconditional.
why it matters
Closes the bridge between the Prop-level signed-orbit order and the Bool nonnegative flag that certificates and display lemmas expose. Downstream, integer_order_certificate packages the closed order surface (including the flag display via nonnegFlag_eq_true_iff); this lemma is the zero-specialization used when comparing against the origin. It is also the rewrite target in recipNonzero_num_zero_le_iff (reciprocal numerator nonnegativity) and in zero_lt_iff_nonnegFlag_and_not_balanced_zero (strict positivity as flag plus not balanced at zero).
In the foundation stack this is pure arithmetic infrastructure under the primitive recognition calculus, not a forcing-chain (T0–T8) step. It keeps order reasoning interchangeable with the structural flag used in later ratio and certificate work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.