signedOrbitEquiv_equivalence
plain-language theorem explainer
Signed-orbit equivalence (the balanced-length relation on pairs of distinction naturals) is an equivalence relation. Anyone constructing the quotient that yields PRC integers cites this fact. The proof is a one-line wrapper reusing the already-proved equivalence of the underlying balanced relation.
Claim. The balanced-length relation on signed orbits is an equivalence relation: it is reflexive, symmetric, and transitive.
background
In the Primitive Recognition Calculus integer layer, a signed orbit is a pair $(p,n)$ of distinction naturals, read as the formal difference $p-n$. Two signed orbits are related by the balanced-length relation when their positive and negative legs match after cancellation of common length (the internal arithmetic that will become integer equality).
The module defines signed-orbit equivalence simply as that balanced relation. Upstream, the balanced relation on signed orbits is already shown to be reflexive, symmetric, and transitive, packaged as a single Equivalence record. The present declaration lifts that fact to the named equivalence used by the quotient construction.
proof idea
One-line wrapper: the goal is Equivalence signedOrbitEquiv, and signedOrbitEquiv is definitionally the balanced relation, so the proof is exactly the upstream theorem that balanced is an equivalence (built from its refl, symm, and trans lemmas).
why it matters
This theorem is the iseqv witness for the setoid on signed orbits. That setoid is the carrier for quotient-native PRC integers: integer equality is the balanced-length relation, and the quotient classes are the integers of the calculus. Without a proved equivalence, the setoid (and therefore the integer type) cannot be formed. It sits in the foundation stack that turns orbit arithmetic into a genuine integer type before later forcing-chain and recognition-composition work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.