le_mul_left_iff_of_nonnegFlag_of_not_balanced_zero
plain-language theorem explainer
Left multiplication by a strictly positive signed orbit preserves the internal order: az ≤ aw if and only if z ≤ w. Order-theoretic arguments in the Primitive Recognition Calculus cite this when cancelling a positive factor. The proof reduces both sides to ℤ via toInt and finishes with linear arithmetic once positivity of a is established.
Claim. Let $a,z,w$ be signed orbits. If $a$ is nonnegative and not balanced with the zero orbit (equivalently $a$ maps to a strictly positive integer), then $a\cdot z \le a\cdot w$ if and only if $z \le w$, where $\le$ is the signed-orbit order and $\cdot$ is signed-orbit multiplication.
background
Signed orbits are the Primitive Recognition Calculus carriers for integers: each has positive and negative orbit lengths, with the internal equivalence balanced meaning $a.pos + b.neg = b.pos + a.neg$ (K4.9). The recovery map toInt sends a signed orbit to an ordinary integer; balanced orbits map to equal integers, and the zero orbit maps to $0$.
The order le on signed orbits is defined so that it agrees with the usual order on integers after toInt. Nonnegativity is tracked by a Boolean flag nonnegFlag, equivalent to $0 \le a.toInt$. The local module builds the full order surface (reflexivity, transitivity, totality, trichotomy, sign flags) needed for an integer-order certificate.
Upstream, balanced_iff_toInt_eq and the nonnegativity flag lemmas connect the orbit-level predicates to integer inequalities; multiplication of signed orbits multiplies the recovered integers.
proof idea
Translate the nonnegativity hypothesis into $0 \le a.toInt$ via the flag equivalence. From $\neg$ balanced$(a,0)$ and balanced_iff_toInt_eq with zero_toInt, deduce $a.toInt \neq 0$, hence $0 < a.toInt$ by omega. Rewrite both order statements with le_iff_toInt_le and both multiplications with mul_toInt, obtaining the integer claim $a\cdot z \le a\cdot w \Leftrightarrow z \le w$ under $a > 0$. Close both directions with nlinarith.
why it matters
This is a cancellation / monotonicity law for the internal signed-orbit order: positive left factors may be cancelled without changing comparisons. It feeds integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed," packaging display lemmas for nonnegativity, flags, and related order facts.
In the Recognition foundation stack, integers are recovered from logic and ledger structure before the forcing chain (T0–T8) and the J-cost calculus. Closing order under multiplication by positive elements is part of showing that the PRC integer layer behaves like ordinary $\mathbb{Z}$, so later mass-ladder and constant derivations can treat comparisons as standard. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.