PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget_of_mixed_reflects
plain-language theorem explainer
Under prime-direction calibration of a ratio character, the reflection form of the mixed-witness bridge implies the control form: prime-axis no-mixing controls arbitrary nonunit no-mixing. Anyone closing the native-cost uniqueness witness split cites this lift. The proof is a pointwise application of the character-level mixed-reflects-to-control lemma under the universal target hypothesis.
Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated has the property that mixed nonunit witnesses reflect down to mixed prime-axis witnesses. Then every such $\chi$ also satisfies: prime no-mixing controls arbitrary nonunit no-mixing.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits used to build a native cost via doubled-trace data. Prime-direction calibration restricts how $\chi$ behaves along prime axes. The witness-split bridge compares two no-mixing statements: one only on prime-axis witnesses, and one on arbitrary nonunit witnesses.
Two target propositions package the same bridge under calibration. The control target says that, for every calibrated character, prime no-mixing already forces nonunit no-mixing. The reflection target says the converse packaging: mixed nonunit witnesses must reflect down to mixed prime-axis witnesses. At the single-character level, the upstream lemma records that reflection implies control by a direct modus-ponens rearrangement.
This declaration lives in the native-cost uniqueness module, where those targets are the composite bridge steps needed before uniqueness certificates can fire.
proof idea
Term-mode proof that unpacks the universal control target. Introduce a character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the given mixed-reflects target at $(\chi,h\chi,h\mathrm{prime})$ to obtain the character-level reflection hypothesis, then feed that into the upstream lemma PRCCharacterPrimeWitnessesControlNonunitWitnesses_of_mixed_reflects, which turns reflection into control for that $\chi$. No extra algebraic work.
why it matters
Closes one direction of the equivalence between the control and reflection packagings of the prime-calibration witness bridge. Downstream, the iff theorem pairs this with the converse lift, and the unconditional proved form of the control target is obtained by feeding the already-proved mixed-reflects target into this lemma.
That proved control target is part of the native-cost uniqueness blocker certificate path and appears in the conditional universal-foundation certificate stack. In Recognition Science terms, the witness split is a gate on the way to uniqueness of the native cost built from the J-cost / doubled-trace character data (the T5 J-uniqueness lineage). Without control under prime calibration, nonunit mixing could escape the prime-axis constraints that pin the cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.