PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_proved
plain-language theorem explainer
Under prime-direction calibration, a ratio character whose prime-axis witnesses never mix also has no mixed nonunit witnesses. Native-cost uniqueness and the nonunit no-mixed split cite this composite bridge. The proof is a one-line term application of the mixed-reflects implication to the already-proved reflection form.
Claim. For every map $\chi$ on ratio orbits that is a ratio character and is prime-direction calibrated, prime witnesses control nonunit witnesses: absence of mixed prime-axis witnesses implies absence of mixed nonunit witnesses.
background
In Primitive Recognition Calculus, ratio characters $\chi$ are structure-preserving maps on ratio orbits. Prime-direction calibration restricts how $\chi$ acts along prime axes. Witnesses record mixing of orbit data; the native-cost uniqueness program needs a split between prime-axis mixing and arbitrary nonunit mixing.
The target proposition is the composite bridge: under prime calibration, prime no-mixing should control arbitrary nonunit no-mixing. Its reflection dual says mixed nonunit witnesses must reflect down to mixed prime-axis witnesses. The module builds native cost uniqueness from J-cost, doubled-trace, and d'Alembert hypotheses on these characters.
Upstream, the reflection form is already proved by reducing to a split target. A separate implication theorem converts any proof of the reflection form into a proof of the control form.
proof idea
One-line term proof. Apply PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_of_mixed_reflects to the already-proved reflection theorem PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_proved. That implication intro's the character and calibration hypotheses, then discharges the control goal via the mixed-reflects lemma on characters. No further casework.
why it matters
Closes the composite witness-split bridge needed for native-cost uniqueness. Downstream, PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget_of_no_mixed_prime_witnesses packages this proved control target with a no-mixed-prime hypothesis into the full nonunit split. The same fact feeds prc_native_cost_uniqueness_blocker_certificate and, through the foundation stack, prc_universal_foundation_conditional_certificate.
In the Recognition forcing chain this sits under uniqueness of the native cost functional (the J-cost side of T5), ensuring calibrated characters cannot hide nonunit mixing once prime axes are clean. It is a proved leaf in the blocker certificate, not scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.