mul_ofOrbit_balanced_scaleByNat
plain-language theorem explainer
Multiplying a signed orbit by the nonnegative orbit of a distinction count is balanced with scaling that orbit by the same count. Order comparisons and sign-flag lemmas for right-multiplication by positive orbits cite this equivalence. The proof is a short rewrite chain through the integer display of signed orbits.
Claim. For every signed orbit $z$ and distinction natural $d$, the product of $z$ with the nonnegative orbit built from $d$ is balanced with the natural scaling of $z$ by $d$: their positive and negative lengths satisfy $a_{+} + b_{-} = b_{+} + a_{-}$, equivalently both sides display the same integer.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of distinction-natural lengths (positive and negative parts). Two signed orbits are balanced when $a_{+} + b_{-} = b_{+} + a_{-}$; this is the internal PRC integer relation, defined only on $\delta$-orbit positions. The bridge theorem states that balance holds if and only if the two orbits display the same integer under the conservative $\mathbb{Z}$ view.
The nonnegative embedding sends a distinction natural $n$ to the signed orbit with positive part $n$ and negative part zero; its integer display is just $n$. Multiplication of signed orbits is defined so that the integer display multiplies: $(\mathrm{mul},a,b).\mathrm{toInt} = a.\mathrm{toInt}\cdot b.\mathrm{toInt}$. Natural scaling of an orbit by $d$ is the matching operation on the display side: its integer value is the product of the orbit's integer with $d$.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). The present lemma equates the two ways of "multiplying by a nonnegative count" before order and flag lemmas use that identification.
proof idea
One short rewrite proof. Replace balance by equality of integer displays via the bridge characterization. Expand the product display with the multiplication law, replace the nonnegative orbit's display by the underlying natural, and expand the scaled orbit's display. Both sides reduce to the same product of integers, so the goal closes.
why it matters
This is the algebraic hinge that lets order and sign structure pass through right-multiplication by a nonnegative orbit. Downstream, nonnegativity and negativity flags of $z\cdot\mathrm{ofOrbit}(d)$ are identified with those of $z$ (for $d\neq 0$) by transporting along this balance. The same fact feeds the comparison lemmas: $\le$, $<$, and $\mathrm{cmp}$ of products against $\mathrm{ofOrbit}(d)$ reduce to the corresponding relations on the factors.
Those pieces assemble into the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed. In the Recognition foundation this is ledger-level bookkeeping on $\delta$-orbits, not yet the J-cost or forcing chain, but it is required scaffolding so later PRC layers can treat signed integers as ordered without leaving the orbit calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.