toRat_mk
plain-language theorem explainer
Converting a ratio-orbit representative to a PRC rational and then to Mathlib ℚ recovers the orbit's own rational display. Anyone transporting PRC rationals into verifier ℚ, or simplifying J-cost and positivity lemmas on the quotient, cites this simp rule. The proof is pure definitional equality (rfl).
Claim. For every ratio orbit $q$ (signed-orbit numerator over a nonzero distinction-nat denominator), if $\mathrm{mk}(q)$ is the PRC rational built from that representative, then its Mathlib rational equals the direct display of $q$: $\mathrm{toRat}(\mathrm{mk}(q)) = (\mathrm{num}(q):\mathbb{Q})/(\mathrm{den}(q):\mathbb{Q})$.
background
In the primitive recognition calculus, rationals are not taken as primitive. A RatioOrbit is a display pair: a signed orbit numerator and a nonzero distinction-nat denominator (K4.7). Its verifier map sends the pair to Mathlib $\mathbb{Q}$ by integer division of the two underlying Nats/Ints.
PRC rationals are the quotient of these displays under cross-multiplication equality. The constructor mk embeds a representative into that quotient; the recovery map toRat on the quotient is defined so that on a pure representative it agrees with the orbit display. Spec tag A5 records that this recovery is a transport wrapper whose internal content is cross-multiplication.
The same pattern already appears one layer down in RationalsFromLogic, where toRat (mk a b hb) = (toInt a : ℚ) / toInt b holds by rfl. The present lemma is the orbit-level analogue.
proof idea
One-line wrapper: rfl. Unfolding mk and the quotient-level toRat reduces both sides to the same RatioOrbit display (q.num.toInt : ℚ) / (q.den.toNat : ℚ), so the equality is definitional. Marked @[simp] for automatic transport in downstream rewrites.
why it matters
This is the basic simp bridge between ratio-orbit representatives and Mathlib ℚ on the PRC rational quotient. Downstream it is used heavily in RationalField: lifting the PRC J-cost to the quotient (onPRCRat), proving that cost equals $(x+x^{-1})/2-1$ on the recovered rational (onPRCRat_toRat), normalizing representatives, and characterizing positivity by 0 < q.toRat. It also feeds unit-fraction displays in RealCompleteness and the round-trip/injectivity API in RationalsFromLogic (fromRat_toRat, toRat_add, toRat_fromRat).
In the forcing chain this sits under the rational substrate on which the unique cost $J(x)=\cosh(\log x)-1$ (T5) and the Recognition Composition Law act. Without a clean toRat ∘ mk identity, J-cost and completeness statements cannot move between orbit displays and the quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.