PRCCharacterPrimeWitnessesControlNonunitWitnesses_of_mixed_reflects
plain-language theorem explainer
If a ratio-orbit character reflects mixed nonunit witnesses into mixed prime-axis witnesses, then prime no-mixing already controls all nonunit witnesses. Cite this when wiring the composite prime-to-nonunit bridge in PRC native-cost uniqueness. The proof is a two-line contrapositive: feed the mixed-nonunit assumption through reflection and discharge against prime no-mixing.
Claim. Let $\chi$ be a map on ratio orbits. Suppose that whenever mixed nonunit witnesses for $\chi$ exist, mixed prime-axis witnesses already exist. Then prime no-mixing controls arbitrary nonunit witnesses: if $\chi$ has no mixed prime witnesses, it has no mixed nonunit witnesses.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator / nonzero-denominator display of a rational (K4.7). A character $\chi$ is a self-map of ratio orbits used to probe native cost uniqueness via directional witnesses along prime and nonunit axes.
After prime witnesses are isolated, a composite bridge is still required: prime no-mixing must force nonunit no-mixing. That control statement is the implication "no mixed prime witnesses $\Rightarrow$ no mixed nonunit witnesses." Its exact reverse packaging is the reflection form: existence of mixed nonunit witnesses already forces existence of mixed prime-axis witnesses. Product propagation does not supply that reverse direction, so the two forms are recorded separately and linked by pure logic.
This module sits in the native-cost uniqueness development for PRC characters (doubled-trace / d'Alembert side), where witness control is the remaining bridge after prime calibration.
proof idea
Pure logical packaging of the contrapositive. Introduce the two hypotheses of the control implication (prime no-mixing, and a mixed-nonunit witness package). Apply the reflection hypothesis to the mixed-nonunit package to obtain a mixed prime-axis witness package, then feed that into prime no-mixing. No arithmetic on orbits or primes is used; the body is a two-line intro/exact chain.
why it matters
Closes one direction of the composite bridge equivalence used throughout PRC native-cost uniqueness. Downstream, it is half of the biconditional identifying control with reflection, and it is the discharge step in the prime-calibration forcing target: once calibration forces the mixed-reflects property, this theorem upgrades that to the control target needed for nonunit witness suppression.
In the broader Recognition forcing picture this is scaffolding inside character uniqueness for the native J-cost (the T5 cost shape), not a new physical law. It keeps the prime-axis isolation step from leaking mixed nonunit counterexamples before the cost is pinned.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.