add_respects_cross
plain-language theorem explainer
Cross-equivalence of ratio orbits is a congruence for addition: if a₁ ~ a₂ and b₁ ~ b₂ under cross-multiplication, then a₁+b₁ ~ a₂+b₂. Anyone building the PRC rational field from δ-orbits cites this to justify lifting addition through the quotient. The proof rewrites to integer cross-products and closes by a two-term linear combination of the hypotheses.
Claim. Let $a_1,a_2,b_1,b_2$ be ratio orbits (signed-orbit numerator over nonzero distinction-nat denominator). If $a_1$ is cross-equivalent to $a_2$ and $b_1$ is cross-equivalent to $b_2$, then the ratio-orbit sums $a_1+b_1$ and $a_2+b_2$ are cross-equivalent.
background
In the Primitive Recognition Calculus, rationals are not taken from Mathlib's $\mathbb{Q}$. A ratio orbit packages a signed orbit numerator with a nonzero distinction-nat denominator. Two such displays are identified by cross-equivalence: $a$ and $b$ are related when the scaled signed orbits $a.\mathrm{num}\cdot b.\mathrm{den}$ and $b.\mathrm{num}\cdot a.\mathrm{den}$ are balanced.
The choice-free hub is the integer characterization: cross-equivalence holds iff $a.\mathrm{num}.\mathrm{toInt}\cdot b.\mathrm{den}.\mathrm{toNat}=b.\mathrm{num}.\mathrm{toInt}\cdot a.\mathrm{den}.\mathrm{toNat}$. That bridge uses only propext and Quot.sound, avoiding Classical.choice. Upstream, signed-orbit addition recovers ordinary integer addition under toInt, and scaling by a distinction-nat multiplies the integer display by the corresponding natural.
Local setting is K4 of the integer/rational layer: build PRC rationals as the quotient of ratio orbits by cross-equivalence, then equip the quotient with field operations.
proof idea
Rewrite both hypotheses and the goal via the integer cross-product characterization. Unfold ratio-orbit addition, then simplify the resulting toInt expressions with signed-orbit addition-to-int, scale-by-nat-to-int, and the recovery theorem that distinction-nat multiplication matches Nat multiplication under toNat. After push_cast, the goal is an equality of integer polynomials in the four cross-products. Close with linear_combination of the two hypotheses, weighted by the products of the opposite denominators' natural values.
why it matters
This is the congruence lemma that lets addition descend to the quotient. Downstream, PRCRat.add is defined by Quot.lift₂ of ratio-orbit addition; both well-definedness obligations call this theorem (once with a reflexivity hypothesis on the fixed argument). Without it, the K4.11 addition on PRC rationals cannot be stated as a total operation on equivalence classes.
In the broader Recognition stack, PRC rationals sit under the arithmetic recovered from primitive distinction and feed later forcing and display layers. The lemma is pure foundation: it does not invoke J-cost, phi, or the T0–T8 chain, but it is part of the choice-light integer spine those layers rely on when they need rational arithmetic internal to the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.