scaleByNat_balanced_zero_of_balanced_zero
plain-language theorem explainer
If a signed orbit is balanced against zero, scaling both legs by any positive distinction keeps it balanced against zero. Order and certificate lemmas in the primitive recognition calculus cite this to show zero is fixed under positive scaling. The proof rewrites through the integer display and multiplies by a natural.
Claim. Let $z$ be a signed orbit (pair of distinction lengths meant as $\mathrm{pos}-\mathrm{neg}$). If $z$ is balanced with the zero orbit, then for every distinction length $d$, the scaled orbit $(\mathrm{pos}\cdot d,\,\mathrm{neg}\cdot d)$ is also balanced with zero.
background
In the primitive recognition calculus, integers are not postulated; they arise as signed differences of $\delta$-orbit lengths. A SignedOrbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $\mathrm{pos}_a+\mathrm{neg}_b=\mathrm{pos}_b+\mathrm{neg}_a$, the internal PRC integer relation (K4.9).
That relation is equivalent to equality of the conservative integer displays: balanced iff toInt values agree. Scaling by a distinction multiplies both legs: $(\mathrm{pos}\cdot d,,\mathrm{neg}\cdot d)$, and the display multiplies accordingly: $(\mathrm{scaleByNat},z,d).\mathrm{toInt}=z.\mathrm{toInt}\cdot d$.
The local module builds the order surface on these signed orbits (reflexivity, totality, sign flags, comparison with zero). Zero is the orbit with both legs trivial; balancing against it means the signed difference is the integer zero.
proof idea
Term-style rewrite proof. First replace both balanced hypotheses/goals by equality of toInt via balanced_iff_toInt_eq. Then rewrite the scaled side with scaleByNat_toInt and the zero side with zero_toInt, substituting the hypothesis that $z.\mathrm{toInt}=0$. A final simp on zero_toInt closes $0\cdot d=0$.
why it matters
Feeds integer_order_certificate, which packages the closed internal signed-orbit order surface (nonneg display, flag display, truncated subtraction, and related comparison lemmas). Without stability of zero under positive scaling, the order certificate could not treat scaled representatives of zero as still zero.
In the Recognition foundation this is bookkeeping for the integer layer under the forcing chain: signed orbit differences must behave like $\mathbb{Z}$ before cost functionals and the eight-tick structure sit on top. It is a small but necessary closure fact for K4-style integer arithmetic internal to PRC, not a physics law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.