sub_toRat
plain-language theorem explainer
Subtraction of ratio orbits is compatible with the verifier map to ordinary rationals: the display of a difference equals the difference of the displays. Anyone transporting orbit-level arithmetic into ℚ (J-cost evaluation, native-cost uniqueness, trace-root candidates) cites this. The proof unfolds subtraction as addition of a negation, rewrites with the add and negate transport lemmas, then closes by ring.
Claim. For ratio orbits $a$ and $b$ (signed-orbit numerator over a nonzero distinction-nat denominator), if $\mathrm{sub}$ is orbit subtraction and $(\cdot)^{\mathbb{Q}}$ is the verifier map to $\mathbb{Q}$, then $(a-b)^{\mathbb{Q}} = a^{\mathbb{Q}} - b^{\mathbb{Q}}$.
background
In the Primitive Recognition Calculus, a ratio orbit is the internal display of a rational: a signed orbit as numerator and a nonzero distinction-nat as denominator (K4.7). The verifier map sends such a pair to the ordinary rational $\mathrm{num}^{\mathbb{Z}}/\mathrm{den}^{\mathbb{N}}$; the module treats this as a transport wrapper whose internal equality is cross-multiplication (spec tag A5).
Orbit arithmetic is built before the verifier: subtraction is defined by adding the negation, addition and negation already have transport lemmas to $\mathbb{Q}$. The local setting is IntegerRational: recovering field operations on these orbit displays so later cost functionals can be stated and compared entirely in the native language, then read out in $\mathbb{Q}$.
Upstream, add_toRat states that addition of ratio orbits displays as rational addition, and negate_toRat states that negation displays as rational negation. Together they reduce difference transport to ordinary ring algebra on $\mathbb{Q}$.
proof idea
Term-mode proof in three steps. Unfold the definition of orbit subtraction (difference is sum with the additive inverse). Rewrite the resulting expression using the already-proved transport lemmas for addition and negation of ratio orbits. The goal collapses to an identity of rational expressions, discharged by ring.
why it matters
This is the subtraction half of the ℚ-transport for ratio-orbit arithmetic. Downstream, the J-cost display on ratio orbits rewrites through it: onRatioOrbit_toRat obtains $(q+q^{-1})/2-1$ in verifier rationals by chaining sub, mul, add, recip, and half transport. That identity is the orbit-level form of the unique cost $J(x)=\cosh(\log x)-1$ forced at T5.
Native-cost selection and uniqueness also depend on it. The linear cost is ruled out because its calibration fails after sub_toRat (the ledger expects the canonical $1/4$ display). Trace-root candidate lemmas in PRCNativeCostUniqueness repeatedly rewrite differences of scaled traces via this equality when proving nonzeroness, reciprocity, and the explicit rational formula for the candidate. Without difference transport, the doubled-trace quadratic target cannot be compared in $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.