PRCPrimeCalibrationForcesMixedNonunitWitnessesReflectPrimeWitnessesSplitTarget_of_reflects
plain-language theorem explainer
Under prime-direction calibration, the composite reflection bridge (mixed nonunit witnesses reflect onto mixed prime-axis witnesses) implies its split packaging: separate identity and reciprocal reflection targets. Native-cost uniqueness and universal-foundation certificates cite this when they need the split form of the no-mixed-witness blocker. The proof is a two-branch constructor that applies the character-level split lemma on each conjunct.
Claim. Assume that for every ratio character $\chi$ that is prime-direction calibrated, mixed nonunit witnesses for $\chi$ reflect down to mixed prime-axis witnesses. Then both halves of the split target hold: the identity mixed-nonunit witness reflects to a prime witness, and the reciprocal mixed-nonunit witness reflects to a prime witness.
background
In the Primitive Recognition Calculus, ratio characters are maps $\chi$ on ratio orbits that encode admissible cost-like data. Prime-direction calibration restricts $\chi$ so that its prime-axis behaviour is fixed; mixed nonunit witnesses are composite (non-prime, non-unit) orbit data that would otherwise obstruct uniqueness of the native cost.
The unsplit target asserts a single composite bridge: under those hypotheses, every mixed nonunit witness reflects down to a mixed prime-axis witness. The split target factors that bridge into an identity half and a reciprocal half, matching how the no-mixed-witness blocker is later packaged.
Upstream, the character-level lemma already turns a single-character reflection hypothesis into the corresponding identity/reciprocal split. This declaration lifts that factorisation from one $\chi$ to the quantified calibration-forced targets.
proof idea
Term-mode constructor on the split target (a conjunction). On the identity branch, introduce $\chi$ with character and prime-calibration hypotheses, apply the unsplit target hypothesis to obtain the character-level reflection property, then feed that into the character-level split lemma and project the first conjunct. The reciprocal branch is identical, projecting the second conjunct of the same character-level split.
why it matters
This is one direction of the equivalence between the composite reflection target and its split form; the sibling converse closes the other direction, and together they give the iff used when certificates choose packaging. Downstream it feeds prc_native_cost_uniqueness_blocker_certificate (the native-cost uniqueness blocker stack) and, via that stack, prc_universal_foundation_conditional_certificate in UniversalFoundation.
In the Recognition framework this sits inside the PRC native-cost uniqueness program that forces the J-cost shape (T5 landmark: $J(x)=(x+x^{-1})/2-1$) by ruling out mixed witnesses once prime calibration is in force. It does not itself prove uniqueness; it only converts the reflection bridge into the split shape the blocker certificate expects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.