abs_eq_zero_iff_toInt_eq_zero
plain-language theorem explainer
For a signed orbit difference z (intended as pos − neg), the internal absolute value is the zero distinction orbit exactly when the verifier integer of z is 0. Order and ring lemmas in IntegerOrder cite this to move between abs-zero and integer-zero without leaving the orbit calculus. The proof is a two-direction tactic argument via abs_toNat and natAbs_eq_zero.
Claim. Let $z$ be a signed orbit (a pair of distinction naturals read as $\mathrm{pos}-\mathrm{neg}$). Then the absolute value of $z$, as a distinction natural, equals the zero distinction natural if and only if the integer display of $z$ is $0$.
background
In the primitive recognition calculus, integers are built before classical $\mathbb{Z}$ is assumed. A SignedOrbit is a pair of distinction naturals $(\mathrm{pos},\mathrm{neg})$ with intended meaning $\mathrm{pos}-\mathrm{neg}$. Distinction naturals themselves come from orbit iteration counts via the forward map toNat from logic naturals.
The absolute value of a signed orbit is the orbit-level absolute difference of its two components, not a classical $|\cdot|$ on $\mathbb{Z}$. The verifier display toInt recovers an ordinary integer from that pair. The bridge lemma abs_toNat states that the natural display of this internal absolute value equals Int.natAbs of the verifier integer: $z.\mathrm{abs}.\mathrm{toNat}=|z.\mathrm{toInt}|_{\mathbb{N}}$.
This module sits in the foundation layer that reconstructs arithmetic from recognition orbits, feeding later order and multiplication facts that must stay internal to signed orbits rather than smuggling classical integer algebra.
proof idea
Bidirectional constructor.
Forward: from $z.\mathrm{abs}=0$, rewrite with toNat_zero to get $z.\mathrm{abs}.\mathrm{toNat}=0$. Transport across abs_toNat to obtain $\mathrm{natAbs}(z.\mathrm{toInt})=0$, then apply Int.natAbs_eq_zero.
Reverse: from $z.\mathrm{toInt}=0$, use injectivity of toNat on distinction naturals. Rewrite the goal with abs_toNat, the hypothesis, Int.natAbs_zero, and toNat_zero to finish.
No case split on sign is needed; abs_toNat already packages the absolute-difference arithmetic.
why it matters
This is the zero-characterization bridge between internal absolute value and the verifier integer. Downstream, IntegerOrder uses it as the first rewrite in abs_eq_zero_iff_balanced_zero (equating abs-zero with balance against signed zero) and throughout the family of product-zero laws: abs_mul_eq_zero_iff, the balanced variants, and the left/right balanced stability lemmas for multiplication.
Those facts keep the no-zero-divisors and comparison-selector story inside signed orbits, which is required before order and ring structure can be treated as recognition-native rather than imported from Mathlib integers. In the broader RS foundation, this is bookkeeping on the integer layer that later supports forcing-chain arithmetic (T0–T8 scaffolding), not a physics claim itself. It closes a small but heavily reused equivalence so later order proofs stay short and uniform.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.