threePrimeDirection_toRat
plain-language theorem explainer
The prime-3 ratio orbit displays as the rational 3 under the verifier map. Anyone evaluating native-cost characters, three-adic twists, or two-three composite directions on the orbit-3 axis cites this as the base evaluation. The proof unfolds the direction constructor and reduces by the general prime-direction display lemma plus the orbit-3 natural value.
Claim. The verifier rational display of the prime-$3$ ratio orbit equals $3$.
background
In the Primitive Recognition Calculus, a ratio orbit is a discrete multiplicative object the verifier can display as a rational. The display map sends an orbit to the quotient of its signed numerator integer by its denominator natural; the module tags this as a transport wrapper whose internal characterization is cross-multiplication.
A prime direction is the ratio orbit built from a prime distinction natural. The general upstream lemma states that such a direction displays exactly as the underlying prime's natural value. The three-orbit is that distinction natural for 3, so the three-prime direction is the specialization at 3.
This lives in the native-cost uniqueness module, which asks whether calibrating a cost character at one prime (typically agreement with the J-cost at 2) forces agreement on other prime axes. The three-adic axis twist and three-to-five rebase characters are the classical counterexamples showing it does not.
proof idea
Short tactic proof. Unfold the definition of the three-prime direction, then rewrite by the general prime-direction-to-rational lemma (any prime orbit displays as its natural value) and the fact that the three-orbit evaluates to the natural number 3. Close with numerical normalization.
why it matters
This simp lemma is the evaluation hook for every three-axis calculation in the uniqueness development. Downstream it discharges the three-adic twist reciprocal identity (the base-3 analogue of the two-adic twist on rational displays), the three-to-five rebase evaluations (including the negative calibration statement that the rebased character fails to match native cost on the three-prime axis), and the composite/mixed two-three direction displays (6 and 3/2).
Those results show that native-cost calibration at one prime does not propagate to other primes. In the broader Recognition Science forcing chain this supports T5 J-uniqueness: once the Recognition Composition Law is imposed, only the J-cost is compatible across all prime axes; characters that agree with J at 2 can still twist or rebase the 3-axis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.