add_toRat
plain-language theorem explainer
Addition of ratio orbits is compatible with the map to ordinary rationals: the rational value of a sum equals the sum of the rational values. Anyone proving that native cost or doubled-trace displays on ratio orbits match classical J-cost arithmetic will cite this. The proof unfolds the orbit sum, reduces via signed-integer and scaling lemmas, then finishes by field simplification and ring normalization.
Claim. For ratio orbits $a$ and $b$ (each an integer numerator over a nonzero orbit denominator), if $\mathrm{toRat}$ sends a ratio orbit to its value in $\mathbb{Q}$, then $\mathrm{toRat}(a+b)=\mathrm{toRat}(a)+\mathrm{toRat}(b)$.
background
In the primitive recognition calculus, rationals are not taken as primitives. A RatioOrbit is a display with a signed-orbit numerator and a nonzero distinction-nat denominator (K4.7). The map toRat reads that display into verifier rationals by casting the signed integer value of the numerator over the natural value of the denominator.
Addition of ratio orbits is defined by the usual cross-multiplication pattern on those orbit components (scale each numerator by the other denominator, add the signed orbits, multiply denominators). The integer layer already has a recovery theorem: signed-orbit addition agrees with integer addition under toInt, and scaling a signed orbit by a distinction-nat multiplies the integer value by that nat.
The local module builds integer and rational arithmetic from logic-level orbits so that later cost and gauge constructions can compute on displays while still comparing to classical $\mathbb{Q}$ and $\mathbb{R}$.
proof idea
Unfold the definitions of ratio-orbit addition and toRat. Rewrite the numerator using signed-orbit addition compatibility (add_toInt) and the two scalings by the opposite denominators (scaleByNat_toInt), and rewrite the product of denominators via toNat_mul.
Record that each denominator casts to a nonzero rational (den_cast_ne_zero). Then field_simp clears the common denominator, push_cast aligns integer and natural casts into $\mathbb{Q}$, and ring_nf finishes the algebraic identity.
why it matters
This is the additive half of the bridge from orbit-level rational arithmetic to classical $\mathbb{Q}$. Downstream cost machinery uses it constantly: cost_display rewrites the native doubled-trace display into the halved-and-shifted rational trace by applying add_toRat (with mul_toRat and unit lemmas). The same rewrite appears in zero-calibration and base hypotheses for sign-gauge and signed-power native costs, and in real-character factorization facts such as monotonicity of the rational trace.
Without additive recovery, one could not identify orbit-native cost displays with the classical J-cost expressions that feed the Recognition Composition Law and the forcing chain. It is infrastructure rather than a physics claim, but it is load-bearing for every gauge-orbit cost theorem that compares displays to real characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.