negativeFlag_mul_eq_false_of_balanced_zero_right
plain-language theorem explainer
Multiplying any signed orbit by an orbit balanced with zero yields a product that is not strictly negative. Order theorists on the Primitive Recognition Calculus integer layer cite this when sealing sign-flag arithmetic under zero multiplication. The proof cases on the negative flag and contradicts the already-proved nonnegativity of the same product.
Claim. For signed orbits $z$ and $w$, if $w$ is balanced with zero (orbit lengths satisfy the internal integer relation $w \equiv 0$), then the product $z \cdot w$ has negative flag equal to false, i.e. $z \cdot w$ is not strictly negative.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: pairs of nonnegative $\delta$-orbit lengths (pos, neg). Two orbits are balanced when $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$; this is the internal equality relation on the integer layer, defined entirely on orbit positions. Zero is the zero orbit, so balanced-with-zero means the orbit represents the integer $0$.
Nonnegativity is a computable Boolean flag: nonnegFlag holds when the negative side is structurally $\le$ the positive side. The negative flag is its Boolean negation (strict negativity as failure of nonnegativity). Multiplication of signed orbits is the ring product on this representation.
The sibling result nonnegFlag_mul_of_balanced_zero_right already shows that multiplying by a zero-balanced orbit forces the product's nonnegativity flag to true. The exclusivity bridge negativeFlag_eq_true_iff_nonnegFlag_eq_false equates the two flags.
proof idea
Term-mode proof by contradiction on the Boolean cases.
First invoke the sibling lemma that the product's nonnegativity flag is true whenever the right factor is balanced with zero. Then case-split on the product's negative flag. The false branch is immediate by reflexivity. The true branch applies the exclusivity iff to deduce that the nonnegativity flag is false, rewrites with the sibling fact, and obtains a Boolean contradiction.
why it matters
This lemma is one of the sign-flag arithmetic facts feeding integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, structural $\le$, absolute difference, and the signed nonnegativity bridge into a single closed order interface.
In the Recognition foundation stack, the integer order on signed orbits is the discrete substrate beneath ledger forcing and the later continuous J-cost calculus. Closing multiplication-by-zero behavior for the negative flag keeps the order total and compatible with the ring structure before any continuum limit is taken. It does not itself touch T5–T8 (J-uniqueness, $\phi$, eight-tick, $D=3$), but it is part of the discrete scaffolding those forcing steps sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.