crossEq_decidable
plain-language theorem explainer
Decidability of cross-multiplication equality on ratio orbits: for any two PRC rational displays, whether numerator–denominator cross products balance as signed orbits is a decidable proposition. Anyone writing case splits or constructive order arguments on the phi-ladder rationals needs this instance. The proof unfolds the definition and hands off to existing decidability of signed-orbit balance.
Claim. For any two ratio orbits $a,b$ (each an integer numerator over a nonzero orbit denominator), the proposition that $a$ and $b$ are cross-equal—i.e. that the signed orbit $a_{\mathrm{num}}$ scaled by $b_{\mathrm{den}}$ balances $b_{\mathrm{num}}$ scaled by $a_{\mathrm{den}}$—is decidable.
background
In the Primitive Recognition Calculus, rationals are not classical fractions of integers. A ratio orbit is a pair of a signed orbit numerator and a nonzero distinction-nat denominator (K4.7). Equality of two such displays is internal: cross-multiplication equality (K4.10) asserts that $a.num$ scaled by $b.den$ balances $b.num$ scaled by $a.den$ as signed orbits, entirely on $\delta$-orbit positions.
That balance relation already carries a decidability instance from the integer-orbit layer. The present declaration only lifts that fact to the named cross-equality predicate on ratio orbits, so downstream order and trichotomy lemmas can branch constructively without classical choice.
The surrounding module develops the strict order ltQ and its trichotomy on these ratio orbits; decidable cross-equality is the equality case of that trichotomy.
proof idea
One-line infrastructure proof. Unfold RatioOrbit.crossEq to expose the underlying SignedOrbit.balanced statement on the two scaled numerators; then infer_instance finds the existing decidability instance for signed-orbit balance. No new arithmetic is proved.
why it matters
Cross-equality is the native equality test for PRC rationals before any embedding into classical $\mathbb{Q}$. Without a decidable instance, constructive proofs of order trichotomy (ltQ_trichotomy and siblings in this module) cannot case-split on whether two ladder positions coincide. That order infrastructure sits under the Grow calculus that feeds mass-ladder comparisons and cost uniqueness in the foundation layer.
No downstream consumers are recorded yet on the graph; the declaration is pure typeclass glue for the ratio-orbit order development. It does not itself touch T5–T8 or the RCL, but it keeps the rational layer of the forcing chain fully constructive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.