PRCCharacterMixedNonunitWitnessesReflectPrimeWitnesses_of_prime_control
plain-language theorem explainer
If a ratio-orbit character has the prime-control bridge (no mixed prime witnesses implies no mixed nonunit witnesses), then mixed nonunit witnesses already force mixed prime-axis witnesses. Anyone closing the native-cost uniqueness bridge after isolating primes cites this. The proof is pure logic: one contrapositive application of the control hypothesis.
Claim. Let $\chi$ be a map on rational orbits. Suppose that absence of mixed prime-axis witnesses for $\chi$ implies absence of mixed nonunit witnesses. Then: if $\chi$ admits both an identity-direction nonunit witness and a reciprocal-direction nonunit witness, it already admits mixed prime-axis witnesses (cross-equality on some prime direction and its reciprocal).
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters $\chi$ act on these orbits; cost uniqueness arguments track how $\chi$ treats prime directions versus general nonunit directions.
Two bridge propositions sit after primes are isolated. Prime control says: if $\chi$ has no mixed prime witnesses, then it has no mixed nonunit witnesses. The reflection form is the reverse direction product propagation does not give: existence of mixed nonunit witnesses forces existence of mixed prime-axis witnesses.
The module builds native-cost uniqueness by forcing characters that match the doubled-trace / $J$-cost structure. These witness-bridge props are the exact composite step still needed once prime witnesses are under control.
proof idea
Pure propositional contrapositive of the control hypothesis. Introduce the mixed-nonunit premise, assume for contradiction that mixed prime witnesses fail, apply control to obtain nonunit-no-mixing, and discharge against the mixed-nonunit assumption. No orbit arithmetic is used; the argument is one by_contra plus modus ponens on hcontrol.
why it matters
Closes one direction of the equivalence between prime control and mixed-nonunit reflection, used immediately by PRCCharacterPrimeWitnessesControlNonunitWitnesses_iff_mixed_reflects. Downstream, prime-calibration targets invoke it to promote a control hypothesis into the reflection target (PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_of_prime_control).
In the Recognition stack this is scaffolding for native-cost uniqueness of the PRC character, which feeds the $J$-cost story (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law). It does not itself force $\phi$ or the eight-tick octave; it only equates two formulations of the prime-to-nonunit witness bridge so later calibration lemmas can choose the more convenient polarity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.