twoThreePrimeMixedDirection_toRat
plain-language theorem explainer
The mixed 2–3 prime direction evaluates to the rational 3/2 under the orbit-to-rational map. Anyone separating mixed prime directions from composite orbits in native-cost uniqueness cites this. The proof unfolds the mixed direction, multiplies the known prime values via mul/recip toRat lemmas, and normalizes.
Claim. Under the canonical map from ratio-orbits to $\mathbb{Q}$, the mixed two–three prime direction equals $3/2$.
background
In the Primitive Recognition Calculus, ratio-orbits package a signed integer numerator over a nonzero distinction-nat denominator, giving a discrete display of positive rationals. The map toRat sends such an orbit to its ordinary rational value.
Multiplication and reciprocal on ratio-orbits are compatible with that map: $(ab)^{\mathbb{Q}} = a^{\mathbb{Q}} b^{\mathbb{Q}}$ and $(a^{-1})^{\mathbb{Q}} = (a^{\mathbb{Q}})^{-1}$. The pure prime directions for 2 and 3 already evaluate to $2$ and $3$ respectively.
The mixed direction is the orbit built by combining those prime directions (product of one with the reciprocal of the other). This module develops uniqueness of the native cost functional; comparing mixed versus composite orientations at the first composite $2\cdot 3$ is a local step in that argument.
proof idea
Term-mode proof. Unfold the definition of the mixed direction, then rewrite with the multiplicative and reciprocal compatibility lemmas for toRat, together with the already-proved evaluations of the pure two-prime and three-prime directions. A final norm_num reduces the resulting rational expression to $3/2$.
why it matters
Feeds the two non-equality lemmas that the mixed direction is not cross-equal to the composite $2\cdot 3$ orbit, nor to that composite's reciprocal. Those lemmas discharge the local orientation obstruction at the first mixed composite: the character image of $2\cdot 3$ cannot be forced to the composite or its reciprocal by the mixed direction alone.
That separation is part of the native-cost uniqueness chain in PRC: only the genuine J-cost character survives the doubled-trace and d'Alembert constraints. Downstream uniqueness of the Recognition Composition Law cost (the T5 J-uniqueness landmark) relies on ruling out such composite confusions early.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.