nonnegFlag_mul_of_balanced_zero_left
plain-language theorem explainer
If a signed orbit is balanced with zero, its product with any signed orbit is nonnegative. Order and arithmetic lemmas on the PRC integer surface cite this to keep the zero-left product inside the nonnegative cone. The proof rewrites through the integer display and finishes by omega on 0 * n ≥ 0.
Claim. Let $z,w$ be signed orbits. If $z$ is balanced with the zero orbit (equivalently $z$ has integer display $0$), then the product orbit $z\cdot w$ has nonnegative flag true, i.e. $0 \le (z\cdot w)^{\mathrm{toInt}}$.
background
In Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (pos, neg) with integer display toInt = pos - neg. Two orbits are balanced when a.pos + b.neg = b.pos + a.neg; by balanced_iff_toInt_eq this is exactly equality of integer displays. The zero orbit has display 0.
Multiplication of signed orbits is defined so that mul_toInt holds: (mul a b).toInt = a.toInt * b.toInt. The computable nonnegative flag is the structural comparison leq neg pos; nonnegFlag_eq_true_iff equates the flag to the classical inequality 0 ≤ toInt.
This module builds the order surface on that integer display: reflexivity, totality, trichotomy, and sign-flag exclusivity. The present lemma is the zero-left absorption fact for the nonnegative cone under multiplication.
proof idea
Term-style rewrite proof. First rewrite the goal with nonnegFlag_eq_true_iff and mul_toInt, turning it into 0 ≤ z.toInt * w.toInt. Then rewrite the balance hypothesis with balanced_iff_toInt_eq and zero_toInt to obtain z.toInt = 0. Substitute and close by omega on 0 ≤ 0 * w.toInt.
why it matters
Closes a basic multiplicative cone fact on the signed-orbit integer order: zero on the left forces the product into the nonnegative region. Downstream, negativeFlag_mul_eq_false_of_balanced_zero_left applies it directly (nonnegative flag true implies negative flag false via exclusivity). It also feeds the broader integer_order_certificate, whose doc states the internal signed-orbit order surface is closed and packages the nonnegative-flag display lemmas.
In the Recognition foundation this sits inside the PRC integer layer that underwrites ledger arithmetic before the forcing chain (T0–T8) and the J-cost calculus. It is pure order/arithmetic scaffolding, not a physics claim, but without it the certificate that the internal order matches the conservative ℤ view would have a hole at zero products.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.