abs_scaleByNat_ne_zero_iff
plain-language theorem explainer
Absolute value of a signed orbit scaled by a natural distinction is nonzero exactly when both the orbit's absolute value and the scale factor are nonzero. Anyone building the signed-orbit order or the integer-order certificate cites this zero-product dual. The proof is a short constructor/contrapositive argument off the companion equality-to-zero biconditional.
Claim. For every signed orbit $z$ and every distinction $d$, the absolute value of $z$ scaled by $d$ is nonzero if and only if both $|z|$ is nonzero and $d$ is nonzero.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction naturals $(p,n)$ read as the formal difference $p-n$. Its absolute value is the orbit position $\mathrm{absDiff}(p,n)$. Scaling by a distinction $d$ multiplies both components: $\mathrm{scaleByNat}(z,d)=(p\cdot d,,n\cdot d)$.
The companion lemma states that the absolute value of a scaled orbit vanishes exactly when either the original absolute value vanishes or the scale factor is zero. That is the zero-product law for this absolute-value/scaling pair. The present statement is its nonzero dual, needed wherever one reasons about strict positivity or nondegeneracy under scaling.
The local module develops the order surface on signed orbits (reflexivity, totality, trichotomy, sign flags) that later feeds the integer-order certificate.
proof idea
Invoke the companion biconditional $\mathrm{abs}(\mathrm{scaleByNat},z,d)=0\leftrightarrow |z|=0\lor d=0$. Split on the desired nonzero equivalence.
Forward: if the scaled absolute value is nonzero, neither disjunct of the zero law can hold, so both $|z|\neq 0$ and $d\neq 0$. Each case is discharged by feeding the corresponding injection into the companion and contradicting the nonzero hypothesis.
Backward: if both factors are nonzero and the scaled absolute value were zero, the companion would force one of the two zero disjuncts, each of which contradicts the joint nonzero assumption.
why it matters
This lemma is a small but necessary nondegeneracy fact on the signed-orbit absolute value under scaling. It is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed: the certificate packages display lemmas for truncated subtraction, order comparison, absolute difference, and signed nonnegativity flags.
Within Recognition Science foundation work, signed orbits are the discrete integer layer beneath the phi-ladder and the forcing chain. Closing their order surface (including zero/nonzero behaviour under scaling) is prerequisite scaffolding for later mass-ladder and constant extractions that treat integer ranks as well-ordered distinctions. The result does not itself touch T5--T8 or the RCL; it keeps the integer substrate consistent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.