cmp_eq_eq_iff
plain-language theorem explainer
Two signed orbits compare as equal exactly when they are balanced (matching net orbit length). Order and arithmetic lemmas on the primitive recognition calculus integers cite this biconditional constantly. The reverse direction is a one-line appeal to the balanced-implies-eq lemma; the forward direction is a short case split on the definition of the comparison selector.
Claim. For signed orbits $a$ and $b$, the internal comparison returns equality if and only if $a$ and $b$ are balanced: $a_{\mathrm{pos}}+b_{\mathrm{neg}}=b_{\mathrm{pos}}+a_{\mathrm{neg}}$.
background
In the primitive recognition calculus, a signed orbit is a pair of distinction-natural lengths (pos, neg), read as the formal difference pos - neg. Two signed orbits are balanced when their lengths match across sides: a.pos + b.neg = b.pos + a.neg. That relation is the internal integer equality of the calculus; it is defined only on δ-orbit positions, not on any external integer display.
The comparison selector is built from that relation and a structural nonnegative flag. It returns equality when the two orbits are balanced; otherwise it inspects the nonnegative flag of the difference b - a and returns less-than or greater-than accordingly. The nonnegative flag itself is the Boolean leq of the two sides of a single signed orbit.
This module develops the order theory of those signed orbits. The present biconditional is the exact bridge between the Boolean/Ordering face of comparison and the Prop-level balanced relation used in algebraic lemmas.
proof idea
Iff introduction. The reverse direction is immediate: apply the already-proved lemma that balanced orbits compare as equal (a one-line simp on the definition of the selector).
The forward direction assumes the selector returns equality, unfolds the selector, and cases on whether the orbits are balanced. The balanced branch is the goal. The unbalanced branch cases further on the nonnegative flag of b - a; both Boolean outcomes make the unfolded selector evaluate to lt or gt, so simp contradicts the equality hypothesis.
why it matters
This is the workhorse characterization of equality in the signed-orbit order. Downstream it is used by left and right translation invariance of comparison under addition, by congruence of comparison under balanced replacements, by the sign-sensitive multiplication rules (nonnegative and negative left/right multipliers), and by the negation-swap rule for comparison.
In the Recognition Science stack this sits inside the foundation layer that reconstructs integer order from pure recognition data (δ-orbits and balance), before the forcing chain reaches J-uniqueness, φ, the eight-tick octave, or D = 3. Closing the equality face of comparison is what lets later arithmetic lemmas treat balanced orbits as interchangeable without dropping into the external integer embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.