PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_of_trace_coherence
plain-language theorem explainer
Prime calibration that forces identity orientation to propagate across prime axes also forbids mixed identity/reciprocal choices on distinct primes. Native-cost uniqueness arguments cite this as one direction of the no-mixing/trace-coherence equivalence. The proof is a short term reduction: trace coherence turns a mixed pair into a self-reciprocal prime direction, contradicting non-self-reciprocality under cross-equality.
Claim. Assume prime cost calibration forces identity orientation to propagate across prime axes (the identity-trace-coherence target). Then the same calibration forbids independent mixed identity/reciprocal choices on different prime axes: every ratio character that is prime-direction calibrated is free of mixed prime orientation.
background
In the Primitive Recognition Calculus, rational data live as ratio orbits: a signed-orbit numerator over a nonzero distinction-orbit denominator. Two orbits are related by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality). Reciprocals of ratio orbits are total, sending zero to zero.
A PRC ratio character is a map on ratio orbits obeying the native multiplicative laws. Prime-direction calibration pins how the character acts on native prime axes. The no-mixing target says calibration must rule out independent identity-versus-reciprocal choices on different primes. The identity-trace-coherence target is the remaining exact obligation: calibration must make identity orientation propagate across prime axes.
This lemma sits in the native-cost uniqueness module, where doubled-trace and d'Alembert structure constrain admissible cost characters before uniqueness is certified.
proof idea
Term-mode proof by unfolding the no-mixing target and deriving a contradiction from a mixed pair. Fix a ratio character that is prime-direction calibrated, and primes $p,r$ with $p$ identity-oriented and $r$ reciprocal-oriented. Apply the assumed trace-coherence target to obtain that $r$ is also identity-oriented. Symmetry then transitivity of cross-equality glue the identity and reciprocal witnesses into a self-equation: the prime direction of $r$ is cross-equal to its own reciprocal. Discharge by the lemma that no prime direction is cross-equal to its reciprocal.
why it matters
This is one half of the equivalence between the no-mixed-prime-orientation target and the prime-identity trace-coherence target; the sibling converse closes the biconditional. Downstream, the sharpened-orientation path uses both local and no-mixed orientation targets to obtain coherent prime orientation, then global orientation, and finally the prime-calibration propagation target that feeds native-cost uniqueness.
The blocker certificate for native-cost uniqueness records the discharged factorization and signed-admissible obligations in this module. In the broader Recognition chain, forbidding mixed prime orientations is part of locking the native cost to the unique J-shape forced at T5, before phi and the eight-tick structure appear. The lemma does not invent new physics; it collapses two residual calibration targets so the uniqueness certificate can treat them as one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.