ratioOrbitOfRat
plain-language theorem explainer
Embeds a classical rational into a ratio orbit (signed numerator orbit over a nonzero distinction-orbit denominator). Cost and gauge-orbit classification cite it to move between verifier rationals and native orbit displays. The body is a structure constructor: ofNat on num/den, with den_ne_zero discharged from the rational denominator axiom.
Claim. For each rational $x \in \mathbb{Q}$, form the ratio orbit whose numerator is the signed orbit built from $|x|$'s numerator (positive and negative parts via $\mathrm{toNat}$) and whose denominator is the distinction-orbit of $x$'s denominator; the denominator is nonzero because $x$'s denominator is nonzero in $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, a ratio orbit is the native display of a rational: a signed orbit numerator over a nonzero finite distinction orbit (K4.7). DistinctionNat is the base-neutral inductive orbit of repeated distinction (zero/succ); ofNat and toNat are the verifier bridges to Lean Nat.
The module PRCNativeCostUniqueness studies uniqueness of native cost on these displays. The doc-comment stresses that this map is not a new PRC primitive: it is a verifier-backed section $\mathbb{Q} \to$ RatioOrbit used to probe whether the character interface already admits a classical rational countermodel.
Upstream, ArithmeticFromLogic.toNat reads iteration counts; Orbit.ofNat/toNat and toNat_zero supply the Nat round-trip used in the denominator nonzeroness proof.
proof idea
Definition by structure fields. The numerator is the signed pair (ofNat of x.num.toNat, ofNat of (-x.num).toNat). The denominator is ofNat of x.den. Nonzeroness: assume den equals DistinctionNat.zero, apply toNat, rewrite with toNat_ofNat and toNat_zero to get x.den = 0, contradict x.den_nz. No external lemmas beyond those simp facts.
why it matters
This section is the bridge that lets classical rationals drive native cost constructions. Downstream, GaugeOrbitFromRealCharacter builds signGaugeNativeCost and signedPowerNativeCost by feeding ratioOrbitOfRat into onRatioOrbit; GaugeOrbitClassification uses it in cost_at_neg ("Negative displays are determined by the positive ones"), degenerate_is_signGauge, exists_nat_exponent, and nontrivial_is_signedPower. RealCharacterFactorization uses it for natOrbit and rationalTrace.
In the Recognition forcing picture this supports uniqueness of the J-cost character on rational displays (T5 J-uniqueness / RCL territory): if the character interface already forces the classical cost on these orbits, rational countermodels are ruled out. It is scaffolding for the native-cost uniqueness argument, not a physics law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.