PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_of_prime_control
plain-language theorem explainer
Under prime-direction calibration of a ratio character, the global control bridge (prime no-mixing controls arbitrary nonunit no-mixing) implies the reflection bridge (mixed nonunit witnesses force mixed prime-axis witnesses). Cited by the native-cost uniqueness blocker and the two-target equivalence. Proof is a one-line specialization of the character-level reflection lemma.
Claim. If, for every ratio character $\chi$ that is prime-direction calibrated, prime-axis no-mixing witnesses control arbitrary nonunit no-mixing witnesses, then for every such $\chi$ mixed nonunit witnesses reflect down to mixed prime-axis witnesses.
background
In the Primitive Recognition Calculus, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ are the algebraic carriers of native cost. Prime-direction calibration pins $\chi$ on the prime axes so that cost uniqueness arguments can reduce general mixing questions to prime data.
Two composite bridge targets package the witness-split story under that calibration. The control target asserts that prime no-mixing controls arbitrary nonunit no-mixing. The reflection target asserts the dual form: if mixed nonunit witnesses exist, then mixed prime-axis witnesses already exist. Both are universal statements over calibrated characters.
Upstream, the character-level lemma already converts a single-character control hypothesis into the corresponding reflection property by contradiction on the mixed-prime side. The present declaration lifts that implication from one character to the quantified target propositions.
proof idea
One-line wrapper. Introduce a calibrated ratio character $\chi$ with the ambient hypotheses of the reflection target. Specialize the assumed control target at $\chi$ to obtain prime-witnesses-control-nonunit-witnesses for that character. Feed the specialized hypothesis into the character-level theorem that turns control into mixed-nonunit-reflects-prime, and discharge the goal.
why it matters
Native-cost uniqueness in PRC needs a clean witness-split bridge under prime calibration. This arrow shows the control packaging implies the reflection packaging, so either form may be used as the working hypothesis.
It is the forward half of the local equivalence between the two targets, and it feeds the native-cost uniqueness blocker certificate as well as the conditional universal-foundation certificate. In the broader Recognition chain it sits inside the foundation layer that forces the unique J-cost (T5) and the self-similar fixed point $\varphi$ (T6), by ensuring calibrated characters cannot hide mixing off the prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.