mul_ofOrbit_right_not_balanced_zero_iff
plain-language theorem explainer
The product of a signed orbit z with a nonnegative orbit d is nonzero (not balanced with zero) exactly when both factors are nonzero. Order and arithmetic lemmas for the internal PRC integer surface cite this zero-product law. The proof is a one-step rewrite of the dual balanced-zero identity, followed by a De Morgan case split.
Claim. For any signed orbit $z$ and any distinction-orbit length $d$, the product $z \cdot \iota(d)$ is not balanced with zero if and only if $z$ is not balanced with zero and $d \neq 0$, where $\iota(d)$ is the nonnegative signed orbit with positive part $d$ and negative part $0$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (Peano-style). A SignedOrbit is a pair of such orbits, read as the formal difference pos − neg. Two signed orbits are balanced when their lengths satisfy a.pos + b.neg = b.pos + a.neg; balancing with zero is the internal notion of vanishing.
The embedding ofOrbit d builds the nonnegative signed orbit ⟨d, 0⟩. Right-multiplication by such an orbit is the PRC stand-in for scaling an integer by a natural. The dual identity already proved in this module states that the product is balanced with zero precisely when either factor vanishes: balanced(z · ι(d), 0) ↔ balanced(z, 0) ∨ d = 0.
This module develops the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). Zero-product control is needed so that nonnegativity and strict inequality interact cleanly with multiplication by nonnegative orbits.
proof idea
One-line rewrite of the dual theorem mul_ofOrbit_right_balanced_zero_iff, which equates balanced(z · ι(d), 0) with balanced(z, 0) ∨ d = 0. The goal is the negated biconditional. After the rewrite, a constructor splits into the two directions of ¬(P ∨ Q) ↔ ¬P ∧ ¬Q: the forward direction discharges each conjunct by feeding the corresponding disjunct into the hypothesis; the reverse direction cases on the disjunction and applies the matching conjunct. No further arithmetic is required.
why it matters
Feeds the closed order surface certificate integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas for truncated subtraction, ≤, absolute difference, and signed nonnegativity flags; zero-product control is part of making those flags and the order relation compatible with scaling by nonnegative orbits.
In the Recognition foundation stack this sits under the Primitive Recognition Calculus integer layer, before ledger forcing and the T0–T8 chain. It is pure internal arithmetic: no appeal to J-cost, φ, or the eight-tick octave. It closes a small but necessary gap so that "nonzero times nonnegative nonzero stays nonzero" is available wherever the order certificate is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.