ofOrbit_mul_balanced_scaleByNat
plain-language theorem explainer
Left-multiplying a signed orbit z by the nonnegative orbit of a distinction count d is balanced with scaling z by d. Anyone proving order or sign invariance under positive left-multiplication on the PRC integer surface cites this. The proof rewrites balanced to equal integer displays and finishes by ring on the toInt identities.
Claim. For every distinction count $d$ and signed orbit $z$, the product $\mathrm{ofOrbit}(d)\cdot z$ is balanced with the pointwise scale of $z$ by $d$: their positive and negative orbit lengths satisfy $a_{+} + b_{-} = b_{+} + a_{-}$, equivalently they display the same integer.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative $\delta$-orbit positions (pos, neg). The internal equivalence is balanced: $a$ and $b$ balance when $a.pos + b.neg = b.pos + a.neg$. That relation is the choice-free PRC stand-in for equality of integers; the bridge theorem states it is equivalent to $a.toInt = b.toInt$ on the conservative $\mathbb{Z}$ display.
Nonnegative orbits are built by ofOrbit: ofOrbit$(n) = \langle n, 0\rangle$, so ofOrbit$(n).toInt = n.toNat$. Multiplication of signed orbits multiplies the displays: $(a\cdot b).toInt = a.toInt\cdot b.toInt$. Scaling by a natural distinction count is the matching unary operation on a single orbit; its display multiplies by that count.
This module develops the order surface on those signed orbits (le, lt, cmp, nonneg/negative flags). The present lemma is the algebraic identification that left-multiplication by a pure nonnegative orbit is the same, up to balance, as scaling.
proof idea
Term-mode, four rewrites then ring. First replace balanced by equality of toInt via balanced_iff_toInt_eq. Expand the product display with mul_toInt, the left factor with ofOrbit_toInt, and the scale with scaleByNat_toInt. The resulting integer identity is $d.toNat \cdot z.toInt = z.toInt \cdot d.toNat$, discharged by ring.
why it matters
This is the balance witness that lets order and sign data pass through left-multiplication by ofOrbit$(d)$. Downstream, nonnegFlag and negativeFlag of the product equal those of $z$ (when $d\neq 0$) by transporting flags across this balanced pair. The same witness feeds le_mul_ofOrbit_left_iff_of_ne_zero, lt_mul_ofOrbit_left_iff_of_ne_zero, and cmp_mul_ofOrbit_left_of_ne_zero, which say positive left-multiplication preserves the order comparison.
Those facts close into integer_order_certificate: "the internal signed-orbit order surface is closed." In the Recognition foundation this is part of building integers and their order from $\delta$-orbit positions alone, before the forcing chain (T5 J-uniqueness through T8 dimension) is applied at the physics layer. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.