signedOrbitSetoid
plain-language theorem explainer
Packages the balanced-length relation on signed orbits as a Mathlib setoid. Anyone forming quotient-native PRC integers cites this. The body is a one-line wiring of the already-proved equivalence into Setoid fields.
Claim. The relation on signed orbits (pairs of distinction-naturals read as $\mathrm{pos}-\mathrm{neg}$) given by balanced lengths, $a_{+} + b_{-} = b_{+} + a_{-}$, is an equivalence relation and therefore a setoid on the type of signed orbits.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction-naturals $(\mathrm{pos},\mathrm{neg})$, intended as the formal difference $\mathrm{pos}-\mathrm{neg}$. Two such pairs are balanced when $a_{+} + b_{-} = b_{+} + a_{-}$; that internal length identity is the PRC-native integer relation, stated entirely on $\delta$-orbit positions rather than on classical $\mathbb{Z}$.
The module builds integers as quotient classes of these signed orbits. The balanced relation is first named as a Prop, then re-exported as the binary relation used for equivalence. This declaration turns that relation into a Mathlib Setoid, the standard carrier for Lean's quotient construction.
Upstream, length of finite traces and ledger balance supply the arithmetic vocabulary; the signed-orbit equivalence proof is already discharged before this packaging step.
proof idea
Definitional packaging, not a proof argument. The relation field is set to the balanced-length predicate on signed orbits; the equivalence-proof field is filled by the already-established theorem that that predicate is reflexive, symmetric, and transitive. No further tactics or algebraic reductions appear.
why it matters
K4.8 in the IntegerRational development: without a setoid there is no quotient type of PRC integers. Downstream, the PRC-integer type is exactly the quotient by this setoid, and the constructor is Quot.mk of a signed orbit. The verifier map from those classes into classical $\mathbb{Z}$ is deliberately left as a later theorem, so this definition keeps the integer layer internal to orbit arithmetic until display is justified.
In the broader Recognition stack this is foundation scaffolding for integer and rational structure built from distinction orbits, not yet the forcing chain (T5–T8) or the mass ladder, but a prerequisite for any PRC-native arithmetic that later feeds those layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.