balanced_scaleByNat_iff_of_ne_zero
plain-language theorem explainer
Scaling two signed orbits by the same nonzero distinction count preserves balance of their orbit lengths. Anyone assembling the internal integer order on Primitive Recognition Calculus cites this cancellation lemma. The proof reduces balance to integer equality, multiplies both sides by the positive scale, and closes both directions by linear arithmetic.
Claim. Let $z,w$ be signed orbits and let $d$ be a nonzero distinction count. Then the scaled orbits $z\cdot d$ and $w\cdot d$ are balanced if and only if $z$ and $w$ are balanced, where balance means $z_{\mathrm{pos}}+w_{\mathrm{neg}}=w_{\mathrm{pos}}+z_{\mathrm{neg}}$.
background
In Primitive Recognition Calculus, integers are carried by signed orbits: each orbit records a positive and a negative distinction length. Two signed orbits are balanced when those lengths match crosswise, $a.pos+b.neg=b.pos+a.neg$. That relation is the internal PRC integer equality, defined only on $\delta$-orbit positions (K4.9).
Scaling by a distinction count multiplies both legs of an orbit by the underlying natural number. The forward map toNat reads that count off the logic-natural iteration; zero is exactly the identity orbit. The present lemma lives in the IntegerOrder layer, which equips signed orbits with a total order and packages display lemmas for the order certificate.
Upstream, balance is already known to be equivalent to equality of the integer embeddings of the two orbits. Scaling acts as ordinary multiplication on that embedding, so nonzero scales are invertible for equality questions.
proof idea
First convert $d\neq 0$ into $d.toNat\neq 0$ by injectivity of toNat and the simp fact that zero maps to $0$. Cast to a positive integer inequality $0<(d.toNat:\mathbb{Z})$ via Nat.pos_of_ne_zero.
Rewrite both sides of the claimed biconditional with balanced_iff_toInt_eq, then unfold scaling on the integer embedding via scaleByNat_toInt. The goal becomes ordinary integer arithmetic: $d\cdot z_{\mathbb{Z}}=d\cdot w_{\mathbb{Z}}$ iff $z_{\mathbb{Z}}=w_{\mathbb{Z}}$ under $d>0$. Both directions finish by nlinarith.
why it matters
The lemma is a cancellation step inside the signed-orbit order surface. Downstream it is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed; that certificate bundles display equalities for truncated subtraction, $\le$, absolute difference, and nonnegativity flags.
In the Recognition foundation stack this sits under Arithmetic-from-Logic and Ledger forcing: balance is the ledger-neutral integer relation before any continuum or physical constant is introduced. It does not itself invoke the forcing chain T5–T8, the Recognition Composition Law, or $\phi$, but it keeps the discrete integer layer coherent so later rungs (mass ladder, eight-tick octave) can quote a closed order surface without external $\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.