PRCCharacterMixedNonunitReciprocalWitnessReflectsPrimeWitness
plain-language theorem explainer
Defines the reciprocal half of mixed-context reflection for a ratio-orbit character χ: if χ admits both an identity-oriented and a reciprocal-oriented nonunit witness, then some prime-axis orbit is sent by χ to its reciprocal under cross-equality. Cited by the split mixed-nonunit reflection package and by prime-calibration forcing targets in native cost uniqueness. Pure propositional interface; no proof body.
Claim. For a map $\chi$ on ratio orbits, the following holds: if there exist nonunit nonzero distinction-naturals $p$ and $r$ such that $\chi$ is identity-oriented at $p$ and reciprocal-oriented at $r$, then there exists a prime orbit $q$ with $\chi(\mathrm{primeDir}(q))$ cross-equal to the reciprocal of $\mathrm{primeDir}(q)$.
background
In the Primitive Recognition Calculus, ratio orbits are the internal stand-in for positive rationals built from signed $\delta$-orbits. Cross-equality (crossEq) is the PRC rational relation: two orbits match when scaled numerators and denominators balance as signed orbits (K4.10). The reciprocal of a ratio orbit flips numerator and denominator.
A ratio character $\chi$ is a map on ratio orbits meant to encode cost-relevant orientation data. Orbit-direction predicates record whether $\chi$ acts as the identity or as reciprocal on the direction associated to a distinction-natural. Nonunit means the natural is not a unit in the distinction arithmetic; prime orbits are the irreducible generators on the prime axis.
This module develops native cost uniqueness for PRC characters. The mixed-context antecedent packages simultaneous identity and reciprocal nonunit witnesses, forcing reflection of orientation data down onto the prime axis. Reciprocal events and the reciprocal automorphism appear upstream as the geometric dual of identity (J-cost minimum at $x=1$).
proof idea
Definitional: the body is the implication Prop itself. Antecedent is a conjunction of two existential witnesses (identity-oriented nonunit and reciprocal-oriented nonunit). Consequent asserts existence of a prime orbit whose prime direction is sent by $\chi$ to its reciprocal under crossEq. No tactics or lemmas; downstream theorems discharge instances of this Prop.
why it matters
Fills the reciprocal half of the mixed-context reflection law needed for native cost uniqueness. Paired with the identity half into the split form PRCCharacterMixedNonunitWitnessesReflectPrimeWitnessesSplit. Downstream, prime-local orientation plus product-display compatibility prove this Prop for genuine ratio characters; a calibration target records that prime-direction calibration should force it for every ratio character. The Pass-25 blocker certificate lists related open factorization targets, so this interface is part of the exact Lean surface still separating full native cost uniqueness from a closed theorem. Framework role: orientation coherence on the prime axis is a prerequisite for identifying the native cost with the unique J-cost (T5) on the recognition ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.