PRCPrimeCalibrationForcesNoMixedPrimeWitnessesTarget_of_no_mixed_prime_orientation
plain-language theorem explainer
Prime cost calibration that forbids mixed identity/reciprocal orientations on prime axes also forbids mixed prime witnesses. Anyone assembling the native-cost uniqueness blocker or the orientation/witness target equivalence cites this one-way implication. The proof is a short term application of the character-level orientation-to-witnesses lemma after instantiating the calibration hypothesis.
Claim. If prime cost calibration forces no mixed prime orientation (for every ratio-orbit character that is prime-direction calibrated, independent identity/reciprocal choices on distinct prime axes are forbidden), then it also forces the existential prime-witness form: no mixed prime witnesses exist for such characters.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio-orbit characters encode how multiplicative structure is read off orbits. Prime-direction calibration pins each prime axis to a preferred orientation (identity versus reciprocal). Two related no-mixing targets package the demand that calibration not allow inconsistent orientation choices across primes.
The orientation target asserts that every prime-direction-calibrated ratio character has no mixed prime orientation: it cannot assign identity on one prime axis and reciprocal on another independently. The witnesses target is the existential form of the same idea: there cannot coexist an identity-oriented prime witness and a reciprocal-oriented prime witness.
Upstream, the character-level lemma already shows that no mixed prime orientation on a fixed character implies no mixed prime witnesses on that character. The present result lifts that implication from single characters to the quantified calibration targets.
proof idea
Term-mode proof. Introduce a ratio-orbit map $\chi$ together with the hypotheses that it is a ratio character and is prime-direction calibrated. Apply the assumed orientation target to those data to obtain no mixed prime orientation for $\chi$. Feed that fact into the character-level lemma PRCCharacterNoMixedPrimeWitnesses_of_no_mixed_prime_orientation, which converts orientation non-mixing into witness non-mixing. The result is exactly the witnesses target.
why it matters
Native-cost uniqueness in Recognition Science needs prime calibration to rule out mixed identity/reciprocal readings on prime axes; otherwise the cost character can factor in non-unique ways. This implication is one half of the equivalence between the orientation target and the witnesses target, so either packaging of the no-mixing demand may be used interchangeably.
Downstream it feeds the native-cost uniqueness blocker certificate and the universal foundation conditional certificate. In the forcing chain it supports the uniqueness side of the J-cost story (T5) by ensuring calibrated prime structure cannot smuggle mixed orientations that would break the Recognition Composition Law reading of the cost. It is a proved bridge, not scaffolding: once the orientation target is available, the witnesses form is free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.