twoThreePrimeCompositeDirection_toRat

In the Primitive Recognition Calculus, ratio data live in RatioOrbit, an integer-rational encoding of positive ratios closed under multiplication and reciprocal. The map toRat sends an orbit to its underlying rational in $\mathbb{Q}$. The product law states that the rational of a product is the product of the rationals.

The two-prime and three-prime directions are the basic axis orbits for the primes $2$ and $3$; their rationals are $2$ and $3$ respectively. The composite direction is defined as the orbit product of those two axes, so it is the natural $2\cdot 3$ generator in the ratio lattice.

This module develops uniqueness of the native cost functional on PRC characters. Distinctness of composite versus mixed two/three images is checked after projecting to rationals, so explicit values such as $6$ are the comparison data.

Term-mode proof. Unfold the definition of the composite direction (product of the two- and three-prime directions). Rewrite with the orbit product law mul_toRat, then substitute the simp facts that the two-prime direction has rational $2$ and the three-prime direction has rational $3$. Finish with norm_num to obtain $2\cdot 3 = 6$.

Feeds the two non-cross-equality lemmas that separate the mixed two/three direction from the composite direction and from its reciprocal. Those lemmas are steps in the native-cost uniqueness chain: if a character's cross-equation identified a mixed axis twist with the plain $2\cdot 3$ composite (or its reciprocal), the cost would not be forced uniquely.

In the broader Recognition framework this is bookkeeping on the discrete ratio lattice that underlies J-cost comparisons and the forcing of the unique cost functional (T5 J-uniqueness and the Recognition Composition Law sit upstream of the cost story). The value $6$ is the plain composite; the mixed image is $3/2$, so rational comparison immediately rules out cross-equality.