PRCCharacterMixedNonunitIdentityWitnessReflectsPrimeWitness
plain-language theorem explainer
Identity half of the mixed-context reflection law for PRC ratio characters: if a character admits both an identity-oriented and a reciprocal-oriented nonunit witness, then some prime-axis direction is fixed up to cross-equality. Native-cost uniqueness proofs and the blocker certificate cite this Prop. It is a pure definition packaging that implication, not a proved theorem.
Claim. For a map $\chi$ on ratio orbits, if there exist nonzero nonunit distinction naturals $p$ and $r$ such that $\chi$ has an identity-oriented witness at $p$ and a reciprocal-oriented witness at $r$, then there exists a prime orbit $q$ with $\chi$ of the prime direction of $q$ cross-equal (via balanced scaled numerators) to that same prime direction.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed numerator orbit over a nonzero distinction-natural denominator. Two ratio orbits are cross-equal when scaled numerators balance under cross-multiplication; that is the internal PRC stand-in for rational equality on $\delta$-orbit positions.
Characters here are maps $\chi$ on ratio orbits. Orientation witnesses record whether $\chi$ acts as the identity direction or the reciprocal direction on a given nonzero nonunit distinction natural. Mixed context means both kinds of nonunit witness are present at once.
The ambient module develops native-cost uniqueness for PRC: forcing the cost functional (ultimately the T5 $J$-cost $J(x)=(x+x^{-1})/2-1$) from character and calibration hypotheses on the orbit lattice. Reciprocal structure appears both as the ledger reciprocal event and as the cost-algebra automorphism $x\mapsto x^{-1}$.
proof idea
No proof body: this is a Prop-valued definition. The antecedent is the conjunction of two existential witnesses (identity-oriented nonunit and reciprocal-oriented nonunit). The consequent asserts existence of a prime orbit whose prime direction is fixed by $\chi$ up to cross-equality. Downstream theorems discharge the Prop under ratio-character, product-display compatibility, and prime-local orientation hypotheses.
why it matters
This is the identity half of the mixed nonunit reflection law used to pin characters down to the prime axis before native cost can be identified with doubled-trace $J$-data. It is conjoined with the reciprocal half in the split reflection Prop, appears as a field obligation in the Pass-25 native-cost uniqueness blocker certificate, and is the conclusion of the prime-calibration forcing target for the identity branch. The sibling theorem under prime-local orientation shows the Prop holds once $\chi$ is a ratio character with product-display compatibility and prime-local orientation. In the broader RS chain this supports T5 $J$-uniqueness by eliminating non-prime mixed orientations that would otherwise allow exotic cost characters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.