scaleByNat
plain-language theorem explainer
Componentwise scaling of a signed orbit difference by a positive distinction-natural: both legs are multiplied by the same d. Integer-order and ratio-orbit developments cite it whenever comparison or absolute value must commute with positive scaling. The body is a two-field structure constructor, not a proof.
Claim. For a signed orbit $z=(p,n)$ (intended meaning $p-n$) and a distinction-natural $d$, the scaled orbit is $(p\cdot d,\, n\cdot d)$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor only). Signed orbits package two such orbits as a difference: a SignedOrbit is a pair (pos, neg) whose intended meaning is pos - neg (K4.6). This is the local stand-in for integers before quotienting by balance.
The surrounding IntegerRational module builds integer and rational structure from these orbit objects rather than from classical ℤ. Scaling by a positive-only orbit position is the primitive that later yields absolute-value multiplicativity and order-invariance under nonzero multipliers.
Upstream, negation on related integer encodings swaps legs (-(a,b)=(b,a) in the logic-integer construction). Here scaling keeps the sign pattern and multiplies both legs, matching the usual rule $k\cdot(p-n)=(kp)-(kn)$ for $k\ge 0$.
proof idea
Definition only: construct a SignedOrbit by setting pos := z.pos * d and neg := z.neg * d. No lemmas are applied; the multiplication is the existing DistinctionNat product from the orbit arithmetic layer.
why it matters
This is the scaling primitive that the integer-order layer hangs on. Downstream, abs_scaleByNat proves absolute value multiplies through scaling; abs_scaleByNat_eq_zero_iff and abs_scaleByNat_ne_zero_iff characterize when the scaled absolute value vanishes; balanced_scaleByNat_iff_of_ne_zero and cmp_scaleByNat_of_ne_zero show balance and comparison are invariant under nonzero scaling; and le_scaleByNat_iff_of_ne_zero plus IntegerOrderCertificate package the order laws. Ratio growth also uses it indirectly via zero_ltQ_iff_num.
In the Recognition foundation, integers and rationals are not imported as axioms: they are reconstructed from distinction orbits. Scaling is the step that lets the phi-ladder and mass/rung arithmetic later treat integer coefficients as orbit operations rather than external ℤ. It does not itself force T5–T8; it supplies the arithmetic substrate those forcing steps sit on once costs and dimensions are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.