PRCCharacterMixedNonunitWitnessesReflectPrimeWitnesses
plain-language theorem explainer
If a ratio-orbit character admits both an identity-oriented and a reciprocal-oriented nonunit witness, then mixed prime-axis witnesses already exist under cross-multiplication equality. Native-cost uniqueness arguments cite this as the reflection (contrapositive) form of the composite bridge, the reverse direction product propagation does not give. The declaration is a pure Prop packaging that implication; no proof content.
Claim. For a map $\chi$ on ratio orbits, write $P(\chi)$ for the proposition: if there exist nonzero nonunit distinctions $p,r$ such that $\chi$ acts in the identity direction on $p$ and in the reciprocal direction on $r$, then there exist prime-orbit distinctions $p',r'$ with $\chi$ fixing the prime direction of $p'$ up to cross-multiplication equality and sending the prime direction of $r'$ to its reciprocal up to cross-multiplication equality.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator (the internal rational display). Two ratio orbits are related by cross-multiplication equality when the scaled signed numerators balance: $a.num\cdot b.den$ matches $b.num\cdot a.den$ as signed orbits. That relation is the PRC-native stand-in for rational equality.
A character here is a self-map $\chi$ on ratio orbits. Directional witnesses record whether $\chi$ acts as the identity orientation or the reciprocal orientation along a given distinction. Nonunit witnesses live off the unit class; prime-axis witnesses live on prime orbits, compared via the prime-direction embedding and cross-multiplication equality.
The local module develops native-cost uniqueness for such characters. The doc-comment frames this Prop as the contrapositive/reflection form of the composite bridge: mixed nonunit witnesses force mixed prime-axis witnesses, the reverse direction not supplied by product propagation.
proof idea
No proof: the declaration is a def whose body is a Prop. It packages a single implication whose hypothesis is the conjunction of an existential identity-oriented nonunit witness and an existential reciprocal-oriented nonunit witness, and whose conclusion is the conjunction of an existential identity-oriented prime-axis witness and an existential reciprocal-oriented prime-axis witness (both under cross-multiplication equality on the prime-direction embeddings). Downstream lemmas discharge or rewrite this named Prop; the definition itself only names the bridge.
why it matters
This Prop is the named reflection half of the mixed-context bridge used throughout native-cost uniqueness. Downstream it is shown equivalent to a split form (separate identity and reciprocal halves), and equivalent to the prime-witnesses-control-nonunit-witnesses statement: prime control implies the reflection law, and the reflection law implies prime control. Those equivalences feed the blocker certificate and the target that prime calibration forces mixed nonunit witnesses to reflect prime witnesses.
In the broader Recognition stack this sits under character-to-cost matching and doubled-trace d'Alembert structure for the native cost. It does not itself invoke T5 J-uniqueness or the RCL, but it constrains which characters can serve as cost carriers before those forcing steps apply. Closing the uniqueness pipeline needs both directions of the bridge; this definition supplies the reverse direction as a first-class hypothesis interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.