PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_no_mixed_prime_orientation
plain-language theorem explainer
If prime cost calibration forbids mixed identity/reciprocal orientations on distinct prime axes, then it forces identity orientation to propagate across all native prime axes (prime-identity trace coherence). Native-cost uniqueness and the universal-foundation certificate cite this implication. The proof is a short intro-and-apply: local prime orientation is already proved, then the character-level no-mix-to-coherence lemma finishes it.
Claim. Assume that every ratio-orbit character $\chi$ that is prime-direction calibrated has no mixed prime orientation (identity on one native prime axis and reciprocal on another is forbidden). Then every such $\chi$ is prime-identity-trace-coherent: if any native prime axis is identity-oriented, all native prime axes lie on the identity branch.
background
In the Primitive Recognition Calculus, cost uniqueness is attacked through ratio-orbit characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$. Prime-direction calibration constrains how $\chi$ acts on native prime axes. Two residual targets remain after local orientation is settled.
The no-mixed-orientation target says calibration must forbid independent identity/reciprocal choices on different prime axes. The prime-identity trace-coherence target says calibration must make identity orientation propagate: one identity-oriented native prime forces every native prime onto the identity branch.
Upstream, local prime orientation under calibration is already proved unconditionally. At character level, local orientation plus no-mix already imply prime-identity trace coherence. This declaration lifts that character lemma to the calibration-target layer.
proof idea
Term-style tactic proof in three steps. Introduce a ratio character $\chi$ together with the ratio-character and prime-direction-calibration hypotheses. Feed $\chi$ into the already-proved local-orientation target to obtain local prime orientation. Apply the same hypotheses to the assumed no-mix target to obtain no mixed prime orientation. Conclude by the character-level lemma that local orientation plus no-mix yield prime-identity trace coherence.
why it matters
This is one direction of the equivalence between the no-mix target and the trace-coherence target under prime calibration. The converse sits beside it; together they collapse two residual blockers into one.
Downstream it is wired into prc_native_cost_uniqueness_blocker_certificate, which packages the remaining uniqueness obligations, and into the universal-foundation conditional certificate. In the Recognition forcing picture this sits under native $J$-cost uniqueness (T5 lineage): characters must not freeload mixed prime orientations if the cost is to be forced to the unique $J(x)=(x+x^{-1})/2-1$ shape. Closing no-mix (or equivalently trace coherence) is the live gate on that uniqueness path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.