twoThreePrimeMixedDirection_not_crossEq_composite
plain-language theorem explainer
The mixed two–three ratio orbit 3/2 is not cross-equivalent to the composite orbit 6. Anyone ruling out two-adic axis twists that preserve local 2·3 orientation cites this separation. The proof rewrites cross-equivalence as rational equality and closes by numerical contradiction.
Claim. The ratio orbit obtained by taking the reciprocal of the prime-2 direction and multiplying by the prime-3 direction (display value $3/2$) is not cross-equivalent, in the sense of balanced scaled numerators and denominators, to the composite orbit formed by multiplying the prime-2 and prime-3 directions (display value $6$).
background
In the Primitive Recognition Calculus, a RatioOrbit is an integer numerator over a nonzero distinction-nat denominator: the internal display of a rational. Two such orbits are related by crossEq when scaled numerators balance under cross-multiplication; by K4.10 this is equivalent to equality of the verifier rationals toRat.
The two-adic obstruction package builds two concrete directions at the first mixed composite. The composite direction is the product of the prime-2 and prime-3 directions, with toRat = 6. The mixed direction forced by a two-adic axis twist keeps the 3-branch and inverts the 2-branch, giving the product of the reciprocal of the 2-direction with the 3-direction, so toRat = 3/2.
This lemma lives in the native-cost uniqueness module: it separates those two orbits so that a character cannot identify them while still obeying the PRC ratio-character axioms.
proof idea
Assume cross-equivalence for contradiction. Rewrite via crossEq_iff_toRat_eq to equality of rational displays. Substitute the two simp lemmas that evaluate the mixed direction to $3/2$ and the composite direction to $6$. Close with norm_num, which rejects $3/2 = 6$.
why it matters
The result is a local arithmetic pin in the two-adic axis-twist obstruction. Downstream, PRCCharacterTwoAdicAxisTwist_two_three_local_orientation_absurd uses it to show that no PRC ratio character can carry a two-adic axis twist and still preserve two–three composite local orientation: identifying the mixed image with the composite would require exactly the cross-equivalence ruled out here.
That absurdity feeds the broader native-cost uniqueness argument and is referenced from the conditional universal-foundation certificate in UniversalFoundation. In the Recognition forcing picture it supports uniqueness of the native cost (the J-cost side of T5) by blocking twisted characters that would otherwise produce a second cost functional on the 2–3 lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.