cmp_mul_right_of_negativeFlag

This module builds the order surface on SignedOrbit, the internal model of integers used by the primitive recognition calculus. Each signed orbit carries boolean sign flags (negativeFlag, nonnegFlag) and a recovery map toInt into ordinary integers. Balance is the equality relation on that surface: two orbits are balanced exactly when their integer images agree.

Three-way comparison cmp returns lt, eq, or gt and is tied to the strict order and balance predicates by the usual iff lemmas. Sibling facts already record that the negative flag is true exactly when toInt is negative, and that negativity is exclusive of nonnegativity and of balance with zero.

The local setting is the ordered-ring fragment of the foundation layer: multiplication of signed orbits must interact with order exactly as integer multiplication does. The companion lemma for a non-zero multiplier already gives balance preservation under right-multiplication; the negative case needs the order-reversing companion proved here.

First convert the negative-flag hypothesis into a.toInt < 0, then deduce that a is not balanced with zero (else toInt would be zero, contradiction by omega).

Case on cmp w z:

• If lt, unpack to lt w z, apply lt_mul_right_iff_of_negativeFlag to get lt (z·a) (w·a), and repack with cmp_eq_lt_of_lt.
• If eq, unpack to balance of w and z, reverse by symmetry, push through balanced_mul_right_iff_of_not_balanced_zero (using non-balance of a with zero), and repack with cmp_eq_eq_of_balanced.
• If gt, unpack to lt z w, apply the same negative right-multiplication iff with arguments swapped, and repack as gt.

The three branches together give equality of the two cmp values.

The declaration is one of the order-multiplication coherence facts needed to close the internal signed-orbit order surface. Its sole recorded consumer is integer_order_certificate, whose doc-comment states that surface is closed and packages display lemmas for truncated subtraction, leq, absolute difference, and signed nonnegativity.

In the Recognition foundation stack this sits under the arithmetic-from-logic development: integers recovered from logic must carry a genuine ordered ring structure before they can support ledger balance, rung arithmetic, and the later forcing chain. Without order-reversal under negative multipliers, the certificate cannot honestly claim that the internal comparison matches integer comparison after multiplication.

No open scaffold remains here: the claim is fully proved and feeds the certificate rather than a hypothesis interface.