le_iff_nonnegFlag_sub
plain-language theorem explainer
On signed orbits, a ≤ b if and only if the computable nonnegative flag of b − a is true. Anyone working the internal integer-order layer or the choice-free ℕ characterization cites this direction flip. The proof is a one-line symmetry of the already-proved flag-to-order lemma with arguments swapped.
Claim. For signed orbits $a,b$ (each a pair of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$), one has $a \le b$ if and only if the structural nonnegative flag of the difference $b-a$ equals $\mathsf{true}$.
background
Signed orbits are the internal integer model in the primitive recognition calculus: a structure with two DistinctionNat sides, intended as $\mathrm{pos}-\mathrm{neg}$. Their 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 (leq of neg against pos), not an abstract Prop.
The sibling lemma nonnegFlag_sub_iff_le already equates the flag of $a-b$ being true with $b \le a$, via reduction to integer comparison and omega. The present statement is the same equivalence written in the conventional $a \le b$ orientation, matching the definition of order as nonnegativity of $b-a$. Upstream, order on bare logic-nats is the usual existential-sum relation; here that idea is lifted to signed differences with an explicit flag.
proof idea
One-line term proof: apply the sibling theorem nonnegFlag_sub_iff_le at arguments $(b,a)$ and take .symm. That sibling rewrites the flag through nonnegFlag_eq_true_iff, sub_toInt, and le_iff_toInt_le, then closes by omega. No new arithmetic is done here; only the biconditional direction is flipped to match the $a \le b$ reading.
why it matters
This is the citation-facing form of the flag characterization of signed-orbit order. Downstream, le_iff_toNat_cf uses the order surface to give a purely ℕ-level, choice-free replacement for le_iff_toInt_le (comparing δ-orbit positions). The module certificate integer_order_certificate packages the closed order surface, including the signed nonnegative-flag display, so this lemma is part of sealing the internal integer-order API.
In the Recognition foundation stack this sits under arithmetic-from-logic and the primitive recognition calculus: integers as signed distinction orbits, ordered by a structural flag rather than classical ℤ. It does not itself touch the forcing chain T0–T8, but it is infrastructure those later layers rely on once mass, ticks, and dimensions are built on the same arithmetic spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.