mk_eq_mk_of_balanced
plain-language theorem explainer
Balanced signed orbits yield the same PRC integer: if two signed orbits satisfy the length-balance relation, their images under the quotient constructor coincide. Anyone working with PRC integers as equivalence classes of orbit differences will cite this. The proof is a one-line application of quotient soundness.
Claim. If $a$ and $b$ are signed orbits (pairs of distinction-naturals intended as $\mathrm{pos}-\mathrm{neg}$) and they are balanced, meaning $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$, then the PRC integers they determine are equal: $[a]=[b]$ in the quotient by the balanced-length relation.
background
In the Primitive Recognition Calculus, integers are not postulated; they are built from signed orbit differences. A signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction-naturals, read as the formal difference $\mathrm{pos}-\mathrm{neg}$.
Two signed orbits are balanced when their lengths cross-match: $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. That relation is the setoid used to form PRC integers as a quotient. The constructor sends a signed orbit to its equivalence class in that quotient.
The same pattern appears upstream in the logic-native constructions of integers and rationals, where sound theorems discharge equality of quotient classes from the underlying additive or multiplicative balance equations. Here the balance equation is stated entirely on $\delta$-orbit positions.
proof idea
One-line term proof: apply Quot.sound to the balanced hypothesis. Because PRC integers are defined as Quot by the signed-orbit setoid whose relation is exactly balanced, the hypothesis is already a proof of relatedness, so the quotient identifies the two constructors.
why it matters
This is the K4.8 identification rule for PRC integers: equal balanced signed orbits determine equal PRC integers. It is the integer-side counterpart of the logic-native sound lemmas for integers and rationals, and it licenses treating the quotient constructor as well-defined on balanced pairs.
No downstream dependents are recorded yet in the graph. The immediate role is local scaffolding for PRC integer arithmetic (the module continues with operations that must respect balanced equivalence). In the broader Recognition foundation it keeps the integer layer internal to orbit data before any verifier display into classical $\mathbb{Z}$ is proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.