signedOrbitEquiv_iff_toInt_eq
plain-language theorem explainer
Two signed orbits are equivalent exactly when their integer displays agree: pos−neg as ℤ. Anyone building the quotient of signed orbits into PRC integers cites this as the setoid bridge. The proof is a one-line application of the balanced-length characterization already proved for the same display map.
Claim. For signed orbits $a,b$ (each a pair of distinction naturals, read as $\mathrm{pos}-\mathrm{neg}$), the balanced-length equivalence $a\sim b$ holds if and only if $a$'s integer display equals $b$'s integer display, i.e. $\mathrm{toInt}(a)=\mathrm{toInt}(b)$ in $\mathbb{Z}$.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction naturals, intended as the difference $\mathrm{pos}-\mathrm{neg}$. The verifier display sends it to ordinary integers by $\mathrm{toInt}(z)=(\mathrm{pos}.\mathrm{toNat}:\mathbb{Z})-(\mathrm{neg}.\mathrm{toNat}:\mathbb{Z})$.
Equivalence of signed orbits is defined as the balanced-length relation: two pairs are related when their positive and negative legs match after cancelling common length (the internal PRC relation). Upstream, K4.9 already proves that this balanced relation is equivalent to equality of the $\mathbb{Z}$ displays: "the bridge from the internal PRC relation to the conservative $\mathbb{Z}$ view."
The present statement simply packages that bridge under the name used for the setoid of quotient-native PRC integers.
proof idea
One-line term wrapper. Because signed-orbit equivalence is definitionally the balanced relation, the claim is identical to balanced_iff_toInt_eq, which is applied directly to $a$ and $b$. No extra rewriting or case splits.
why it matters
This is the setoid bridge for quotient-native PRC integers (K4.8/K4.9). Downstream, injectivity of the display map on the quotient (toInt_injective) and the quotient toInt itself rely on equivalence coinciding with equal integer values, so distinct PRC integers get distinct verifier displays.
In the broader foundation stack, integers are recovered from logic and recognition structure rather than postulated; this lemma locks the internal balanced relation to the conservative $\mathbb{Z}$ view before rationals and further arithmetic are built. It does not itself touch the forcing chain T0–T8, but it sits in the integer layer those later constructions consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.