cmp_mul_left_of_negativeFlag
plain-language theorem explainer
Left multiplication by a negative signed orbit reverses three-way comparison: cmp(a·z, a·w) equals cmp(w, z). Anyone assembling the integer order surface from recognition primitives cites this flip law. The proof converts the negative flag to a strict integer inequality, rules out balance with zero, then cases on cmp(w,z) and applies the matching left-multiplication lemmas.
Claim. Let $a,z,w$ be signed orbits. If $a$ is negative (its negative flag is true), then $\mathrm{cmp}(a\cdot z,\, a\cdot w)=\mathrm{cmp}(w,\, z)$.
background
Signed orbits are the internal carriers of integers in the primitive recognition calculus: each orbit has a recovery map to Int, a three-way comparison cmp valued in {lt, eq, gt}, and boolean sign flags. The negative flag is true exactly when the recovered integer is strictly negative. Balance is the equality relation on orbits (recovered integers agree); it is the eq case of cmp.
The local module builds the full order surface on these orbits: reflexivity, transitivity, trichotomy, and the usual links between flags and inequalities (e.g. negative flag iff strictly below zero). Multiplication of signed orbits must interact with order exactly as integer multiplication does.
Upstream ingredients used here include the equivalence of the negative flag with toInt < 0, the characterization of cmp cases via strict order and balance, and the left-multiplication lemmas for negatives: strict inequality reverses under left mult by a negative, and balance is preserved under left mult by any non-zero orbit.
proof idea
First transport the hypothesis: negative flag on $a$ yields $a.\mathrm{toInt}<0$, hence $a$ is not balanced with zero (else the recovered integer would be zero, contradiction by omega).
Case on cmp w z:
- lt: unpack to $w<z$, apply the reverse direction of
lt_mul_left_iff_of_negativeFlag, then repack viacmp_eq_lt_of_lt. - eq: unpack to balance of $w$ and $z$, symmetrize, push balance through left mult by the non-zero $a$ via
balanced_mul_left_iff_of_not_balanced_zero, repack withcmp_eq_eq_of_balanced. - gt: unpack to $z<w$, reverse under left mult by negative $a$ (arguments swapped), repack with
cmp_eq_gt_of_gt.
Each branch is a short transport through the corresponding iff.
why it matters
This is one of the algebraic order laws required to close the signed-orbit order surface. Downstream it is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed: the certificate packages display lemmas for truncated subtraction, nonnegativity, absolute difference, and the signed flags.
In the Recognition foundation stack, integers and their order are not imported from Mathlib as primitives; they are recovered from logic and ledger structure (IntegersFromLogic, ArithmeticFromLogic, ledger balance). The multiplication-order interaction must therefore be proved internally. The negative left-multiplication flip is the last classical sign case after the positive and zero cases, completing trichotomous compatibility of mult with cmp.
No forcing-chain landmark (T5–T8, RCL, phi) is directly at stake; this sits one layer below, in the arithmetic substrate those later steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.