scaleByNat_pos
plain-language theorem explainer
Scaling a signed orbit difference by a positive orbit multiplies the positive leg by that same orbit. Anyone working with integer/rational arithmetic on distinction orbits cites this as the positive-component projection of scale-by-nat. The proof is pure definitional equality (rfl).
Claim. For any signed orbit difference $z=(z_{+},z_{-})$ and any distinction orbit $d$, the positive component of the scaled orbit satisfies $(z\cdot d)_{+}=z_{+}\cdot d$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero/successor), the native stand-in for natural numbers. A SignedOrbit is a pair of such orbits intended as the difference $z_{+}-z_{-}$ (K4.6).
Scaling is defined componentwise: scaleByNat z d returns the signed orbit with positive leg $z_{+}\cdot d$ and negative leg $z_{-}\cdot d$. The product on distinction orbits is the monoid operation inherited from the orbit arithmetic layer.
This module builds integer and rational structure on those orbits so later density and comparison lemmas can talk about ratios without leaving the native type.
proof idea
One-line definitional proof. Unfolding scaleByNat makes the positive field equal to z.pos * d by construction, so rfl closes the goal. Marked @[simp] so later rewrites project the scaled positive leg automatically.
why it matters
Feeds the comparison bridge ltQ_iff_toNat in Grow.RatioOrbitDenseMediant, which rewrites rational-orbit strict order into a pure inequality on toNat of the four legs after cross-multiplication. Without a simp fact that scaling multiplies the positive component, those cross terms do not reduce cleanly.
In the Recognition foundation this is bookkeeping on the integer layer under signed orbit differences, not a forcing-chain landmark. It keeps the K4.6 signed-orbit arithmetic aligned with the later mediant/density arguments that grow rational orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.