balanced_mul_ofOrbit_left_iff_of_ne_zero
plain-language theorem explainer
Left multiplication by a nonzero positive orbit preserves the balanced relation on signed orbits. Anyone assembling the internal integer order from Primitive Recognition Calculus cites this cancellation law. The proof rewrites balance as integer equality, multiplies through by a strictly positive coefficient, and cancels with linear arithmetic.
Claim. Let $d$ be a nonzero distinction count and let $z,w$ be signed orbits. Writing $d^+$ for the positive signed orbit of length $d$, the pair $(d^+\cdot z,\, d^+\cdot w)$ is balanced if and only if $(z,w)$ is balanced, where balance means $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$.
background
In Primitive Recognition Calculus, integers are carried by signed orbits: pairs of nonnegative orbit lengths (positive and negative parts). Two signed orbits $a,b$ are balanced when $a.pos + b.neg = b.pos + a.neg$. That relation is the internal integer equality, defined entirely on $\delta$-orbit positions (K4.9).
Multiplication of signed orbits acts on those lengths; the map that sends a distinction count $d$ to its positive orbit embeds the nonnegative naturals. The integer reading toInt turns a signed orbit into an ordinary $\mathbb{Z}$ value, and balance is equivalent to equality of those integers.
This module builds the order surface on that integer layer. The local setting is the closed certificate that the signed-orbit order is fully displayed by the underlying distinction arithmetic.
proof idea
Rewrite both sides of the biconditional with the characterization that balance means equal toInt values. Push toInt through the two multiplications and through the positive embedding of $d$, so the claim becomes
$$d_{\mathbb{Z}}\cdot z_{\mathbb{Z}} = d_{\mathbb{Z}}\cdot w_{\mathbb{Z}} \iff z_{\mathbb{Z}} = w_{\mathbb{Z}}.$$
From $d\neq 0$ deduce $d.toNat\neq 0$ by injectivity of toNat and the zero case, then cast to a strictly positive integer coefficient. Both directions of the equivalence are then immediate from nlinarith.
why it matters
The theorem is a left-cancellation law for the internal integer equality under positive scaling. It is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed: nonnegativity, flags, truncated subtraction, and absolute difference all display correctly on the distinction layer.
Without cancellation of nonzero positive multipliers, balance would not be stable under the monoid action that embeds $\mathbb{N}$ into signed orbits, and the order certificate could not treat scaled comparisons as faithful. In the broader Recognition stack this sits in the foundation arithmetic that precedes the forcing chain (T0–T8): integers must already be well-formed before J-cost uniqueness, $\varphi$, the eight-tick octave, or $D=3$ are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.