lt_mul_left_iff_of_nonnegFlag_of_not_balanced_zero
plain-language theorem explainer
Left multiplication by a strictly positive signed orbit preserves strict order: az < aw if and only if z < w. Order theorists and anyone building the PRC integer-order certificate cite this as the strict-order half of positive scaling. The proof reduces both sides to ℤ via toInt, obtains 0 < a.toInt from the nonneg flag and non-balance-with-zero, then finishes by nlinarith.
Claim. Let $a,z,w$ be signed orbits. If $a$ is nonnegative and not balanced with zero (equivalently $a.toInt > 0$), then $a\cdot z < a\cdot w$ if and only if $z < w$, where $<$ and $\cdot$ are the internal signed-orbit strict order and multiplication.
background
Signed orbits are the Primitive Recognition Calculus carriers for integers: each has positive and negative δ-orbit lengths, with internal equality given by balance $a.pos + b.neg = b.pos + a.neg$. The recovery map toInt sends a signed orbit to an ordinary integer; balance with zero is exactly toInt = 0, and the nonneg flag is exactly 0 ≤ toInt.
Strict order on signed orbits is defined so that it matches ordinary < after toInt. Multiplication of signed orbits likewise pushes forward to integer multiplication. The local module builds the full order surface (reflexivity, totality, trichotomy, sign flags) needed to treat these carriers as ordered integers inside PRC, without leaving the δ-orbit language.
Upstream, balanced_iff_toInt_eq and the nonneg-flag characterizations supply the bridge from flag/balance hypotheses to integer inequalities; lt_iff_toInt_lt and mul_toInt are the two transport lemmas used here.
proof idea
Translate the nonneg flag into $0 \le a.toInt$. From $\neg$ balanced with zero and balanced_iff_toInt_eq (plus zero_toInt), deduce $a.toInt \ne 0$, hence $0 < a.toInt$ by omega. Rewrite both sides of the claimed biconditional via lt_iff_toInt_lt and mul_toInt, obtaining the integer statement $a.toInt \cdot z.toInt < a.toInt \cdot w.toInt \leftrightarrow z.toInt < w.toInt$. Close both directions with nlinarith using positivity of $a.toInt$.
why it matters
Positive left-scaling of strict order is a standard ordered-ring axiom; here it is proved entirely on signed orbits so the PRC integer layer does not smuggle classical ℤ order. Downstream, cmp_mul_left_of_nonnegFlag_of_not_balanced_zero lifts the same hypotheses to the three-way comparison function, and integer_order_certificate packages the closed order surface ("The internal signed-orbit order surface is closed"). That certificate is part of the foundation stack that forces arithmetic structure before the T0–T8 chain (J-uniqueness, φ, eight-tick octave, D = 3) is read off recognition cost. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.