ratioOrbit_add_congr
plain-language theorem explainer
Addition of ratio orbits respects the cross-multiplication equivalence: equivalent summands yield equivalent sums. Anyone assembling native cost functionals or RCL identities on PRC rational displays cites this. The proof is a short rewrite chain through the rational verifier: cross-equality is toRat equality, and addition of orbits adds the displays.
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 $a_1+b_1$ is cross-equivalent to $a_2+b_2$.
background
In the Primitive Recognition Calculus, a ratio orbit is the internal display of a rational: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Cross-equivalence is the PRC-native equality relation on those displays: two ratio orbits are related when the scaled numerators balance as signed orbits under cross-multiplication (K4.10). That relation is designed to live entirely on $\delta$-orbit positions, without presupposing classical $\mathbb{Q}$.
The bridge to ordinary arithmetic is the verifier map toRat. Upstream, cross-equivalence is equivalent to equality of rational displays, and addition of ratio orbits is compatible with addition of those displays: $(\mathrm{add},a,b).\mathrm{toRat}=a.\mathrm{toRat}+b.\mathrm{toRat}$. The present lemma packages that compatibility as a congruence statement for the internal relation itself.
The ambient module develops uniqueness of native cost functionals on these ratio displays, including character-generated costs and the Recognition Composition Law identities they must satisfy.
proof idea
Rewrite both hypotheses and the goal along the biconditional that cross-equivalence iff equality of toRat displays. Then replace each sum's display by the sum of displays via the addition-compatibility lemma, twice. The two rational equalities from the hypotheses finish the goal by substitution. No case splits and no induction; pure transport along the verifier.
why it matters
Native cost uniqueness needs addition to be well-defined on the quotient of ratio orbits by cross-equivalence. This congruence is the algebraic hinge used when discharging the native-cost hypothesis packages for the zero-flat, two-adic-generated, and absolute-value-generated costs, and when proving that character-generated costs satisfy the canonical RCL identity on products and quotients.
In the broader Recognition chain, the RCL is the functional equation that forces the J-cost (T5: $J(x)=(x+x^{-1})/2-1$). Congruence lemmas like this keep that equation internal to PRC orbit arithmetic rather than smuggling classical field identities. Downstream parents include the native-hypothesis theorems for those generated costs and the canonical RCL statement for costs built from ratio characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.