scaleByNat_neg
plain-language theorem explainer
Scaling a signed orbit by a distinction natural acts componentwise on its negative part: the neg field of the scaled orbit equals the original neg field multiplied by that natural. Anyone simplifying signed-orbit arithmetic before comparison or density arguments will cite this. The proof is pure definitional equality (rfl) from the componentwise definition of scaleByNat.
Claim. Let $z$ be a signed orbit (a pair of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$) and let $d$ be a distinction natural. Then the negative component of the orbit obtained by scaling $z$ by $d$ equals the product of the negative component of $z$ with $d$: $(\mathrm{scale}(z,d))_{\mathrm{neg}} = z_{\mathrm{neg}}\cdot d$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor only). A SignedOrbit (K4.6) is a pair of such orbits, intended as the difference $\mathrm{pos}-\mathrm{neg}$, the local stand-in for an integer before quotienting to logic integers.
Scaling is defined componentwise: scaleByNat z d replaces each component by its product with $d$ (positive-only orbit multiplication). Negation on related integer and rational constructions swaps or signs components (-(a,b)=(b,a) on logic integers; -(a/b)=(-a)/b on logic rationals), but this lemma only exposes the neg field of the scaled pair.
The module sits under Foundation.PrimitiveRecognitionCalculus and builds integer/rational structure from orbits, importing orbit arithmetic so later density and order facts can talk about cross-multiplied numerators and denominators.
proof idea
One-line definitional proof. Unfolding scaleByNat gives a signed orbit whose neg field is definitionally z.neg * d. The two sides of the equality are therefore identical by rfl; the @[simp] attribute makes that reduction available to the simplifier.
why it matters
Small but load-bearing simp fact in the K4.6 signed-orbit layer. Downstream, ltQ_iff_toNat in Grow.RatioOrbitDenseMediant rewrites rational-orbit comparison into a numeric inequality on toNat of positive and negative numerator/denominator parts; componentwise scaling identities keep those rewrites honest when orbits are dilated.
In the broader Recognition stack this is pre-physics scaffolding: integers and rationals are reconstructed from distinction orbits before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) and the mass ladder. It does not itself force a constant; it keeps the arithmetic of signed differences coherent so later mediant-density and comparison lemmas can land.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.