cmp_mul_right_of_nonnegFlag_of_not_balanced_zero

Signed orbits are the internal integer carriers of the primitive recognition calculus. Balance is the equality relation on that carrier: two orbits are balanced when they represent the same integer. The internal comparison selector cmp is defined from balance and the nonnegativity flag of the difference, not from any external integer display: it returns eq on balance, otherwise lt or gt according to the sign of the difference.

The nonnegativity flag marks the closed half-line of nonnegative orbits. The hypothesis that $a$ is not balanced with zero excludes the zero orbit, so together the two assumptions say $a$ is strictly positive. Upstream, right-multiplication by such an $a$ already preserves balance both ways (balanced_mul_right_iff_of_not_balanced_zero) and preserves strict order both ways (lt_mul_right_iff_of_nonnegFlag_of_not_balanced_zero). This theorem lifts those two facts to the three-valued comparison selector.

Term-mode case split on cmp z w.

• If lt: convert via cmp_eq_lt_iff to lt z w, push through lt_mul_right_iff_of_nonnegFlag_of_not_balanced_zero, then re-encode with cmp_eq_lt_of_lt.
• If eq: convert via cmp_eq_eq_iff to balance of $z$ and $w$, push through balanced_mul_right_iff_of_not_balanced_zero, then re-encode with cmp_eq_eq_of_balanced.
• If gt: convert via cmp_eq_gt_iff to lt w z, apply the same strict-order iff with arguments swapped, then re-encode with cmp_eq_gt_of_gt.

No new arithmetic is proved here; the three Ordering cases are pure transport along the already-established iff lemmas.

The parent consumer is integer_order_certificate, which asserts that the internal signed-orbit order surface is closed: display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity all line up with the orbit primitives. Homogeneity of cmp under positive right-multiplication is one of the algebraic closure facts that certificate packages.

In the Recognition foundation stack this sits inside PrimitiveRecognitionCalculus, where integer order is rebuilt from recognition orbits rather than assumed from classical $\mathbb{Z}$. It is not itself a forcing-chain landmark (T0–T8), but it is infrastructure those later layers rely on once integers and their order are available as derived objects. Without positive-multiplier order preservation, the certificate could not treat orbit multiplication as order-compatible arithmetic.