twoPrimeDirection_toRat
plain-language theorem explainer
The distinguished prime-axis direction along the orbit two displays as the ordinary rational 2. Anyone computing two-adic twists, two-three composites, or prime-orientation coherence in the PRC native-cost uniqueness development cites this as a simp fact. The proof unfolds the definition and reduces by the general prime-direction display lemma plus the natural value of the orbit two.
Claim. Let $d_2$ be the ratio orbit obtained as the prime direction of the orbit two. Under the verifier display map from ratio orbits to $\mathbb{Q}$, one has $\mathrm{toRat}(d_2)=2$.
background
In the Primitive Recognition Calculus, ratio orbits carry the native multiplicative structure before recovery to ordinary rationals. The display map sends a ratio orbit to $\mathbb{Q}$ by the quotient of its integer numerator and natural denominator; the internal characterization is cross-multiplication (spec tag A5).
A prime direction is the ratio orbit attached to a distinction-natural that is a prime orbit. The constant for the orbit two is the two-prime direction: the prime direction of that orbit. Upstream, the general display lemma already identifies any prime direction with the natural value of its prime, and a separate simp fact records that the orbit two has natural value 2.
The surrounding module develops uniqueness of the native cost (the $J$-cost) from character hypotheses on ratio orbits, including coherent prime orientation and two-adic axis twists.
proof idea
Short tactic proof. Unfold the definition of the two-prime direction (it is exactly the prime direction of the orbit two). Rewrite by the general prime-direction display lemma, which replaces the direction by the natural value of its prime, and by the fact that the orbit two has natural value 2. Close the resulting numeral equality with norm_num.
why it matters
This simp identity is the base case for every native computation that multiplies or reciprocates the two-axis inside PRC cost uniqueness. Downstream it is used by: the two-adic axis-twist character branch (rewriting the twist at two against the reciprocal of this direction); the two-three composite and mixed direction displays (toRat equals 6 and $3/2$); the mismatch theorem for two-prime composite mixed images under $J$-cost; and the argument that a prime-orientation-coherent character vanishes at zero.
In the Recognition Science forcing chain it sits under the foundation for $J$-uniqueness (T5) and the Recognition Composition Law, by pinning the rational display of the first prime axis used to force native cost characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.