signedOrbitEquiv
plain-language theorem explainer
Signed-orbit equivalence identifies two signed orbit differences when their positive and negative lengths balance crosswise: a₊ + b₋ = b₊ + a₋. Anyone constructing the PRC integer quotient or comparing verifier displays cites this relation. The body is a one-line alias of the balanced-length predicate on signed orbits.
Claim. For signed orbits $a=(a_+,a_-)$ and $b=(b_+,b_-)$ (each a pair of distinction-natural lengths, intended as $a_+-a_-$), declare $a\sim b$ if and only if $a_++b_-=b_++a_-$.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair of distinction-natural lengths (pos, neg), read as the formal difference pos - neg. These are the raw carriers before quotienting to PRC integers.
Two such pairs are related by the balanced-length predicate when the cross sums of lengths agree: a.pos + b.neg = b.pos + a.neg. That identity is the internal integer relation on δ-orbit positions; it does not yet mention a verifier map into ℤ.
This module builds quotient-native integers from those pairs. The present declaration names the balanced relation as the equivalence used for that quotient (K4.9).
proof idea
One-line definitional alias: the relation is exactly SignedOrbit.balanced on the two arguments. No tactics or lemmas are invoked; the meaning is inherited wholesale from the balanced-length equation.
why it matters
This is the named relation that turns signed orbits into a setoid. Downstream, signedOrbitEquiv_equivalence packages reflexivity, symmetry, and transitivity (via balanced_equivalence), and signedOrbitSetoid installs it as the setoid relation for quotient-native PRC integers (K4.8).
The companion characterization signedOrbitEquiv_iff_toInt_eq equates the internal balance relation with equality of verifier displays toInt, so the quotient classes match integer values. In the Recognition foundation this is the discrete integer step under the primitive recognition calculus, before rationals and the forcing chain landmarks (T5–T8) that sit higher in the stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.