mul_balanced_zero_iff_of_balanced_right
plain-language theorem explainer
If two signed orbits are balanced, right-multiplication by either yields a product balanced with zero exactly when the other does. Developers of the PRC integer order surface cite this when transporting zero-tests across balanced representatives. The proof rewrites both sides through the toInt bridge and substitutes the balanced hypothesis.
Claim. Let $a,b,b'$ be signed orbits. If $b$ and $b'$ are balanced (equivalently $b$ and $b'$ display the same integer), then $a\cdot b$ is balanced with zero if and only if $a\cdot b'$ is balanced with zero.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-nats (pos, neg) with intended meaning pos - neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; this is the internal PRC integer relation, defined entirely on δ-orbit positions (K4.9).
The bridge to the conservative integer view is balanced_iff_toInt_eq: balanced pairs are exactly those with equal toInt displays. Multiplication of signed orbits is compatible with that display: (mul a b).toInt = a.toInt * b.toInt. The zero orbit has toInt = 0.
This lemma lives in the IntegerOrder module, which builds the order and sign-flag surface on top of IntegerRational arithmetic so that the internal signed-orbit calculus can stand in for ordinary integer order without leaving the PRC vocabulary.
proof idea
Short rewrite proof. Both sides of the target biconditional are rewritten by balanced_iff_toInt_eq, then mul_toInt on each product and zero_toInt, reducing the claim to
a.toInt * b.toInt = 0 ↔ a.toInt * b'.toInt = 0.
The hypothesis hb is rewritten by the same balanced-to-toInt bridge, and the resulting equality b.toInt = b'.toInt is substituted to finish.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, leq, absolute difference, and signed nonnegativity flags; zero-tests under multiplication must be stable under balanced representatives for those flags and order relations to be well-defined on the quotient.
Within Recognition Science foundation work this is bookkeeping on the PRC integer layer that underwrites later forcing and ledger constructions: without transport of zero across balanced right factors, the signed-orbit model would not faithfully mirror integer arithmetic. It does not itself touch T5–T8 or the RCL; it is infrastructure those layers rely on once integers are internalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.