axisTwistCharacter_toRat
plain-language theorem explainer
The rational display of the axis-twist character on a distinction orbit and a ratio orbit equals the rational axis-twist of their verifier displays. Anyone proving the orbit-level twist is a PRC ratio character, or that it fixes off-axis primes and inverts the on-axis prime, cites this transport. Proof is a one-line unfold plus the ratio-orbit-of-rational round-trip through the rational display.
Claim. For every finite distinction orbit $p$ and every ratio orbit $q$, if $C(p,q)$ denotes the ratio-orbit realization of the $b$-axis twist with $b$ the natural value of $p$, then the rational display of $C(p,q)$ equals the rational axis-twist of $b$ and the rational display of $q$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Its verifier map toNat reads the iteration count as a Lean natural. A RatioOrbit is an integer numerator over a nonzero distinction-orbit denominator; its display toRat is the corresponding rational (spec tag A5: a transport wrapper whose internal law is cross-multiplication).
The axis-twist character packages the rational $b$-axis twist at the orbit level: it sends $(p,q)$ to the ratio orbit obtained by applying the rational axis-twist to $p$'s natural value and $q$'s rational value, then lifting back via ratioOrbitOfRat. This module develops native cost uniqueness for PRC, including character and doubled-trace presentations of cost.
The lemma is the coherence statement that the orbit-level character, once displayed as a rational, recovers the underlying rational twist. Upstream, the forward maps toNat (from logic naturals and from distinction orbits) and toRat supply the verifier side of that bridge.
proof idea
One-line term proof. Unfold the definition of the axis-twist character, which is exactly ratioOrbitOfRat applied to the rational axis-twist of the two displays. The goal reduces to the round-trip identity that displaying ratioOrbitOfRat r as a rational recovers $r$, applied to $r = $ the rational axis-twist at those displays. No case split and no arithmetic.
why it matters
Native cost uniqueness needs an orbit-level ratio character for each prime axis twist. This transport is the bridge those character proofs use when they rewrite through rational equality.
It is cited by three siblings: the theorem that the axis-twist character is a PRC ratio character; the off-axis identity (cross-equality with the prime direction when the prime differs from the axis); and the on-axis reciprocal (cross-equality with the reciprocal of the prime direction), which rewrites via crossEq_iff_toRat_eq and this lemma. Those facts feed the character-trace matching and doubled-trace d'Alembert path toward uniqueness of the native cost.
In the broader RS forcing picture this sits under the foundation layer that isolates the unique cost before T5 J-uniqueness and the RCL are invoked at the continuum level. It does not itself force $J$ or $\varphi$; it keeps the discrete character honest under rational display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.