twoThreePrimeMixedDirection_not_crossEq_composite_recip
plain-language theorem explainer
The mixed two–three prime ratio orbit is not cross-equivalent to the reciprocal of the composite direction 2·3. Cited when excluding two-adic axis twists that would reverse local 2–3 orientation for PRC ratio characters. Proof reduces cross-equivalence to rational equality of verifier displays and closes by concrete arithmetic.
Claim. The mixed two–three prime direction (as a ratio orbit) is not related by cross-multiplication to the reciprocal of the composite direction $2\cdot 3$. Equivalently, their rational displays are unequal: the mixed direction does not equal $(2\cdot 3)^{-1}$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display built from a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equivalence (crossEq) is the internal PRC relation: two orbits match when the cross-multiplied signed orbits balance, i.e. $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ balances $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$. Upstream, this is proved equivalent to equality of the rational verifier maps: crossEq a b iff $a.\mathrm{toRat}=b.\mathrm{toRat}$.
Reciprocal on ratio orbits is total (zero maps to zero) and satisfies $(\mathrm{recip},a).\mathrm{toRat}=(a.\mathrm{toRat})^{-1}$. The composite direction here is the product of the prime-2 and prime-3 directions, i.e. the first mixed composite $2\cdot 3$ in the two-adic obstruction analysis of native cost uniqueness.
This module develops uniqueness of the native cost functional from PRC ratio characters and doubled-trace/d'Alembert constraints; the two–three axis is the first place composite directions can twist orientation relative to pure prime axes.
proof idea
Term-mode proof by contradiction. Assume cross-equivalence of the mixed direction with the reciprocal of the composite direction. Rewrite the assumption via crossEq_iff_toRat_eq to equality of rational displays. Expand with the concrete toRat lemmas for the mixed direction, for recip, and for the composite $2\cdot 3$ direction. The resulting rational equality is false by norm_num.
why it matters
Blocks a concrete rational identification that would let a two-adic axis twist reverse local 2–3 orientation while still looking like a PRC ratio character. Downstream it is used by PRCCharacterTwoAdicAxisTwist_two_three_local_orientation_absurd, which shows that a character with a two-adic axis twist cannot satisfy the two–three composite local-orientation constraint.
That absurdity feeds the broader native-cost uniqueness story in this module and is among the dependencies of prc_universal_foundation_conditional_certificate in UniversalFoundation. In framework terms it is bookkeeping on the rational skeleton beneath J-cost uniqueness (T5) and the Recognition Composition Law: composite directions must not collapse to reciprocals of mixed prime ratios, or the character-to-cost bridge fails on the first non-prime rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.