scaleByNat_congr_of_balanced
plain-language theorem explainer
If two signed orbits are balanced (same internal integer value), scaling both by the same positive distinction keeps them balanced. Order and certificate lemmas cite this to show comparison is homogeneous under positive scaling. The proof rewrites balance as integer equality and multiplies both sides by the scale factor.
Claim. Let $z,w$ be signed orbits (pairs of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). If $z$ and $w$ are balanced, i.e. $z_{\mathrm{pos}}+w_{\mathrm{neg}}=w_{\mathrm{pos}}+z_{\mathrm{neg}}$ (equivalently $z$ and $w$ display the same integer), then for every distinction natural $d$ the scaled orbits $z\cdot d$ and $w\cdot d$ are balanced.
background
In the Primitive Recognition Calculus integer layer, a SignedOrbit is a pair of distinction naturals $(\mathrm{pos},\mathrm{neg})$ with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $a.pos+b.neg=b.pos+a.neg$; this is the internal PRC integer relation (K4.9), defined only on $\delta$-orbit positions.
That relation is equivalent to equality of the conservative integer displays: balanced iff toInt agrees. Scaling by a distinction natural multiplies both components: $(z.scaleByNat,d).pos=z.pos\cdot d$ and likewise for neg. The companion identity is $(z.scaleByNat,d).toInt=z.toInt\cdot(d.toNat:\mathbb{Z})$.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). The present lemma is the congruence of balance under common positive scaling.
proof idea
Term-mode rewrite proof, three steps. First rewrite the balanced hypothesis and goal via balanced_iff_toInt_eq, so the claim becomes equality of integer displays after scaling. Then rewrite both sides with scaleByNat_toInt, obtaining $z.toInt\cdot d.toNat=w.toInt\cdot d.toNat$. The hypothesis $z.toInt=w.toInt$ finishes it. No case splits or classical choice.
why it matters
Feeds cmp_scaleByNat_of_ne_zero, which shows the signed-orbit comparison is invariant under nonzero scaling, and is listed among the ingredients of integer_order_certificate ("The internal signed-orbit order surface is closed."). Without balance-congruence under scale, the order would not be homogeneous on the $\phi$-ladder integer display.
In the Recognition foundation this sits under the ledger/PRC integer bridge: balance is the choice-free internal stand-in for integer equality before the forcing chain (T5 J-uniqueness onward) uses the cost calculus. It closes a small but necessary algebraic step so the certificate can treat scaled orbits as the same integer class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.