nonnegFlag_mul_of_balanced_zero_right
plain-language theorem explainer
Multiplying any signed orbit by a zero-equivalent orbit yields a nonnegative product under the structural nonnegativity flag. Order and arithmetic lemmas on the PRC integer surface cite this when zero annihilates under multiplication. The proof rewrites to integer display, substitutes the zero value, and finishes by omega on 0 ≤ 0.
Claim. For signed orbits $z$ and $w$, if $w$ is balanced with the zero orbit (equivalently $w$ has integer display $0$), then the product $z \cdot w$ has nonnegative flag equal to true, i.e. $0 \le (z \cdot w)^{\mathrm{toInt}}$.
background
In the Primitive Recognition Calculus integer layer, a SignedOrbit packages two distinction-natural counts (positive and negative sides) and displays as an ordinary integer via 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, so balance with the zero orbit means the display is zero.
The nonnegative flag is the structural Boolean DistinctionNat.leq z.neg z.pos. Upstream, nonnegFlag_eq_true_iff identifies the flag with the verifier inequality 0 ≤ z.toInt. Multiplication of orbits is defined so that mul_toInt holds: (mul a b).toInt = a.toInt * b.toInt.
This module builds the order surface on that integer display (reflexivity, totality, trichotomy, sign-flag exclusivity). The local claim is the zero-annihilation half of nonnegativity under multiplication.
proof idea
Term-mode 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 w.toInt = 0. Substitute that equality and close 0 ≤ z.toInt * 0 by omega.
why it matters
Closes a multiplicative edge case on the signed-orbit order surface: zero on the right forces a nonnegative product flag. Downstream, negativeFlag_mul_eq_false_of_balanced_zero_right applies it directly (nonnegativity implies the negative flag is false via the exclusive sign-flag lemmas). Both feed the package theorem integer_order_certificate, whose doc states the internal signed-orbit order surface is closed.
In the Recognition foundation this is bookkeeping for the PRC integer model before the forcing chain (T0–T8) and J-cost calculus. It does not itself force φ, eight-tick structure, or dimension; it keeps the discrete integer order coherent so later recognition arithmetic can quote a certified order surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.