abs_ne_zero_of_toInt_ne_zero
plain-language theorem explainer
If a signed orbit difference evaluates to a nonzero integer, its absolute orbit position is not the zero distinction. Integer-arithmetic and PRC cost-uniqueness proofs cite this when they need a nonzero denominator or absolute value from a nonzero integer display. The argument is a one-line contrappositive through the absolute-value/toInt zero equivalence.
Claim. Let $z$ be a signed orbit difference (pair of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$). If the integer display $z^{\mathbb{Z}}:=n_{\mathrm{pos}}-n_{\mathrm{neg}}$ is nonzero, then the absolute orbit position $|z|$ is not the zero distinction natural.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A SignedOrbit is a pair of such orbits, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Its integer display is $z^{\mathbb{Z}}=(n_{\mathrm{pos}}:\mathbb{Z})-(n_{\mathrm{neg}}:\mathbb{Z})$, and its absolute value is the orbit absolute difference of the two components.
The module builds integer and rational structure from these orbit objects so later PRC cost and ratio arguments can stay native to distinction arithmetic. Immediately upstream sits the biconditional that absolute value is the zero distinction if and only if the integer display is zero; the present lemma is the nonzero direction packaged for direct application.
proof idea
Term-mode contrappositive. Assume $|z|$ equals the zero distinction. Apply the forward direction of abs_eq_zero_iff_toInt_eq_zero to conclude $z^{\mathbb{Z}}=0$, contradicting the hypothesis. No case split on signs is needed; the iff already equates the two zero notions.
why it matters
Feeds three parents: the sibling abs_ne_zero_of_not_balanced_zero (nonzero absolute value from failure of balance with zero), PRCSignedRatioDecompositionTarget_proved (nonzero numerator integer when decomposing signed ratios), and signedQuotient_signCanonical_of_divides (sign-canonical quotients under a nonzero divisor of the absolute value).
In the foundation layer this is bookkeeping for K4.6 signed orbits, not a forcing-chain landmark. It keeps absolute-value nonzeroness aligned with the integer display so PRC native cost uniqueness can treat denominators and quotients without dropping back to classical $\mathbb{Z}$ axioms at each step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.