PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_of_split
plain-language theorem explainer
If the mixed-nonunit reflection target holds in split form (identity half and reciprocal half separately), then it holds in the combined form: every prime-direction-calibrated ratio character has mixed nonunit witnesses reflecting to mixed prime-axis witnesses. Cited when discharging the composite bridge blocker for native cost uniqueness. Proof is a short intro that packages the two split halves into the character-level join lemma.
Claim. Assume the split target: every prime-direction-calibrated ratio character $\chi$ has both (i) mixed nonunit identity witnesses reflecting to mixed prime-axis witnesses and (ii) mixed nonunit reciprocal witnesses reflecting likewise. Then the unsplit target holds: for every ratio character $\chi$ that is prime-direction calibrated, mixed nonunit witnesses of $\chi$ reflect down to mixed prime-axis witnesses.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ are the algebraic carriers of cost. Prime-direction calibration restricts $\chi$ so that its action on prime axes is fixed in the native normalization. Mixed nonunit witnesses are composite (non-prime, non-unit) ratio data that would otherwise obstruct uniqueness of the native cost functional.
The reflection target asserts that any such mixed nonunit witness for a calibrated character must already be visible on mixed prime-axis witnesses. The module splits this into an identity half and a reciprocal half, matching the two legs of the ratio-orbit symmetry. Upstream, the character-level join lemma packages a split pair of reflection properties into the single mixed-nonunit reflection property for one fixed $\chi$.
proof idea
One short tactic proof. Introduce the character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the character-level join lemma PRCCharacterMixedNonunitWitnessesReflectPrimeWitnesses_of_split, feeding it the pair formed by evaluating the two conjuncts of the split target hypothesis at $(\chi, h\chi, h\mathrm{prime})$. No further arithmetic or case analysis.
why it matters
This is the split-to-combined direction of the mixed-nonunit reflection bridge under prime calibration. Downstream it is half of the iff linking the split and unsplit targets, and it is the applicator in PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesTarget_proved, which discharges the target from the already-proved split form. That proved target feeds the native-cost uniqueness blocker certificate and, further out, the conditional universal-foundation certificate. In the Recognition forcing picture this is bookkeeping on the composite bridge that keeps native cost uniqueness aligned with the J-cost uniqueness step (T5) rather than a new physical axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.