scaleByNat_not_balanced_zero_iff
plain-language theorem explainer
Scaling a signed orbit by a distinction length yields a nonzero integer exactly when the original orbit is already nonzero and the scale factor is nonzero. Order and certificate proofs cite this to keep nonzeroness under positive scaling. The argument is a one-line rewrite to the positive balanced-zero iff, then De Morgan on the resulting disjunction.
Claim. For a signed orbit $z$ and a distinction length $d$, $z$ scaled by $d$ is not balanced with zero if and only if $z$ is not balanced with zero and $d \neq 0$.
background
In the Primitive Recognition Calculus, integers are built from signed orbits: a SignedOrbit is a pair of distinction lengths (pos, neg) with intended meaning pos - neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; balancing against zero therefore means the orbit represents the integer zero.
scaleByNat multiplies both legs by a (nonnegative) distinction length $d$, so the integer value scales by the natural number that $d$ denotes. The sibling theorem scaleByNat_balanced_zero_iff already records the positive form: the scaled orbit balances zero exactly when the original does or the scale factor is zero. The present statement is the complementary nonzeroness form used by the integer-order surface.
The local module develops the order structure on these internal integers (reflexivity, totality, trichotomy, sign flags) entirely on $\delta$-orbit data, without external $\mathbb{Z}$.
proof idea
Term-mode proof. Rewrite the goal with scaleByNat_balanced_zero_iff, which turns the left-hand side into the negation of a disjunction. The forward direction splits the conjunction and discharges each conjunct by feeding the corresponding disjunct into the negated hypothesis. The reverse direction cases on the disjunction coming from the rewritten balanced-zero statement and applies the matching conjunct. Pure propositional De Morgan; no arithmetic lemmas beyond the rewrite.
why it matters
Feeds integer_order_certificate, which asserts that "the internal signed-orbit order surface is closed." Nonzeroness under scaling is needed so that the order and sign-flag displays remain coherent when orbits are multiplied by distinction lengths: a nonzero integer stays nonzero under nonzero scaling, matching ordinary $\mathbb{Z}$.
Within Recognition Science this sits in the foundation layer that forces discrete ledger structure before the T0–T8 chain (J-uniqueness, $\phi$, eight-tick octave, $D=3$). Closing the integer-order certificate keeps the PRC integer model self-contained, so later mass-ladder and cost arguments can treat signed orbits as genuine integers without external axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.