cmp_scaleByNat_of_ne_zero

In the primitive recognition calculus, integers are represented as signed orbits rather than as a bare verifier display. The internal comparison cmp returns Ordering.eq exactly when the two orbits are balanced (same signed length), otherwise it reads the nonnegative flag of the signed difference to decide lt or gt. It is deliberately independent of any external integer encoding.

Scaling an orbit by a distinction natural multiplies its magnitude by that natural count. The companion facts used here say that, for nonzero scale factor $d$, the strict order $z<w$ is equivalent to the scaled strict order, and that balance is preserved under common scaling. Those two preservation properties are what make the three-way selector invariant.

The local module builds a full order surface on signed orbits (reflexivity, totality, trichotomy, sign flags) as part of forcing arithmetic from recognition structure, upstream of the closed integer-order certificate.

Term-mode proof by cases on cmp z w.

• If the comparison is lt, convert to the strict-order proposition via cmp_eq_lt_iff, push the inequality through lt_scaleByNat_iff_of_ne_zero (using $d\neq 0$), and reassemble with cmp_eq_lt_of_lt.
• If eq, convert to balance via cmp_eq_eq_iff, apply scaleByNat_congr_of_balanced, and reassemble with cmp_eq_eq_of_balanced.
• If gt, swap the arguments, reduce to the strict-order case as above, and reassemble with cmp_eq_gt_of_gt.

No new arithmetic is invented; each arm is a pure transport along already-proved scale and comparison characterizations.

This is a workhorse invariance lemma for the signed-orbit order. Downstream it is applied directly by the left and right multiplication-comparison theorems: multiplying both sides on the left (resp. right) by a fixed nonzero orbit factor reduces to scaling by the underlying distinction natural, so order is preserved under that multiplication. Those facts feed the closed integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed."

In the broader Recognition Science foundation, integer order is not postulated; it is forced from recognition orbits and ledger balance. Homogeneity of comparison under nonzero scaling is exactly the step that lets the forced order behave like the usual integer order under multiplication by positive naturals, which is required before mass-ladder and tick-count constructions can treat integer ranks as order-theoretic rather than merely combinatorial.