PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_iff_trace_coherence
plain-language theorem explainer
Prime cost calibration forbids mixed identity/reciprocal orientations on distinct prime axes if and only if it forces identity orientation to propagate as trace coherence across those axes. Native-cost uniqueness and the universal-foundation certificate cite this equivalence to collapse two blocker formulations into one. The proof is the term-mode pairing of the two already-proved one-direction implications.
Claim. The assertion that every prime-direction-calibrated ratio character has no mixed prime orientation is equivalent to the assertion that every such character is prime-identity trace-coherent: identity orientation on one native prime axis forces identity orientation on every other native prime axis.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative structure is read as cost. Prime-direction calibration restricts $\chi$ on native prime axes so each axis is oriented either as identity or as reciprocal. The no-mixed-orientation target demands that these choices cannot be chosen independently: once one prime axis is identity-oriented, no other prime axis may sit on the reciprocal branch.
The companion target is prime-identity trace coherence: identity orientation must propagate across all native prime axes. Both targets are universal statements over ratio characters that already satisfy the character axioms and prime-direction calibration. They sit inside the native-cost uniqueness development, whose goal is to force the cost functional toward the unique $J$-shape fixed by the Recognition Composition Law.
Upstream, each direction of the equivalence is already a theorem: trace coherence implies no mixed orientation by applying coherence to a reciprocal witness and using a self-identity contradiction; no mixed orientation implies trace coherence by reducing to a local no-mixing lemma already proved for calibrated characters.
proof idea
Term-mode biconditional: the proof is exactly the pair of the two one-direction lemmas. Left-to-right applies PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_no_mixed_prime_orientation, which introduces a calibrated character and invokes the local no-mixed-orientation lemma already established for that character. Right-to-left applies PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_of_trace_coherence, which, given an identity prime and a reciprocal prime witness, feeds the identity into trace coherence to obtain identity on the second axis and derives the contradiction that closes no-mixing. No further algebra is done at this site.
why it matters
This equivalence is the hinge that lets the native-cost uniqueness development treat "no mixed prime orientation" and "prime-identity trace coherence" as interchangeable blockers. Downstream, the witness-form variant is obtained by transiting through this iff, and both feed the native-cost uniqueness blocker certificate that packages zero-calibrated factorization results. The same fact is listed among the inputs to the universal-foundation conditional certificate, tying PRC calibration hygiene into the broader foundation stack.
In framework terms it is bookkeeping on the path to $J$-uniqueness (T5): mixed prime orientations would allow non-canonical cost characters incompatible with a single self-similar fixed point. Collapsing the two targets removes a duplicate obligation before uniqueness and the phi-ladder mass formula are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.