scaleByNat_toInt
plain-language theorem explainer
Scaling a signed orbit difference by a distinction natural multiplies its recovered integer by that natural. Anyone working in the Primitive Recognition Calculus integer layer cites this when moving between orbit scaling and ordinary ℤ arithmetic. The proof expands both sides via the product recovery map and closes by ring.
Claim. For any signed orbit $z=(p,n)$ (meaning $p-n$) and any distinction natural $d$, the integer recovered from the componentwise scaled orbit equals the product of $z$'s recovered integer with the natural underlying $d$: $(\mathrm{scale}(z,d))^{\mathbb{Z}} = z^{\mathbb{Z}}\cdot d^{\mathbb{N}}$.
background
In the Primitive Recognition Calculus, integers arise as signed orbit differences. A signed orbit is a pair of distinction naturals $(pos,neg)$ with intended meaning $pos-neg$. The recovery map sends the pair to the ordinary integer $pos.toNat-neg.toNat$.
Scaling by a distinction natural multiplies both components: $\mathrm{scale}(z,d)=(pos\cdot d,,neg\cdot d)$. Distinction naturals recover ordinary naturals via the forward iteration-count map, and multiplication on distinction naturals agrees with ordinary multiplication under that map (the recovery theorem for products).
This lives in the IntegerRational foundation module, which builds integer and rational structure from $\delta$-orbit positions without presupposing classical $\mathbb{Z}$.
proof idea
Both sides are expanded explicitly: the left becomes $((pos\cdot d).toNat)-((neg\cdot d).toNat)$ in $\mathbb{Z}$; the right is $(pos.toNat-neg.toNat)\cdot d.toNat$. Each product is rewritten by the recovery theorem that $toNat$ preserves multiplication. After pushing the natural multiplications into integer casts, the identity is pure integer arithmetic and closes by ring.
why it matters
This is the bridge that lets absolute-value and order facts on signed orbits commute with scaling. Downstream it is used by abs_scaleByNat, the zero and balanced characterizations under scaling, the order-scaling equivalences (le/lt iff after nonzero scale), and translation invariance of the delta-native ratio order (leQ_add_right). Those lemmas sit in the integer-order and grow modules that underwrite comparison of ratio orbits, a prerequisite for cost and ladder comparisons later in the foundation stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.