PRCCharacterPrimeReciprocalWitnessGlobalizes
plain-language theorem explainer
Defines the property that a ratio-orbit character globalizes reciprocal orientation across prime axes: if χ sends any native prime direction to its reciprocal (under cross-equality), then it does so for every native prime. Cited in the native-cost uniqueness block when discharging no-mixed-prime-orientation and two-prime forcing lemmas. Pure propositional packaging; no proof content.
Claim. For a map $\chi$ on ratio orbits, the following holds: if there exists a native prime $p$ such that $\chi$ of the prime direction of $p$ is cross-equal to the reciprocal of that direction, then for every native prime $r$, $\chi$ of the prime direction of $r$ is cross-equal to the reciprocal of that direction.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit objects built from signed $\delta$-orbits. Two orbits are identified by cross-equality: $a$ and $b$ satisfy crossEq when the scaled numerators balance as signed orbits ($a.\mathrm{num}\cdot b.\mathrm{den}$ vs $b.\mathrm{num}\cdot a.\mathrm{den}$). Reciprocal swaps numerator and denominator in the orbit sense, matching the ledger reciprocal event (source/target swap with inverse ratio) and the cost-algebra reciprocal automorphism.
A ratio character $\chi$ assigns to each orbit another orbit. On prime axes one can ask whether $\chi$ preserves the identity orientation or flips to the reciprocal. Local character laws (multiplicativity, reciprocal compatibility) do not by themselves relate orientation choices on distinct primes. The module packages native-cost uniqueness hypotheses around doubled-trace and d'Alembert structure for such characters.
This definition isolates the reciprocal branch of that missing cross-prime link: a single reciprocal witness on one calibrated prime forces reciprocal orientation on all calibrated primes.
proof idea
Definitional abbreviation only. The body is the implication $$(\exists,p\ \mathrm{prime}:\ \chi(\mathrm{primeDir},p)\ \sim\ \mathrm{recip}(\mathrm{primeDir},p))\ \Rightarrow\ (\forall,r\ \mathrm{prime}:\ \chi(\mathrm{primeDir},r)\ \sim\ \mathrm{recip}(\mathrm{primeDir},r)),$$ with $\sim$ as cross-equality. No tactics or lemmas are applied.
why it matters
This is the reciprocal-branch form of prime no-mixing inside native-cost uniqueness. Downstream, assuming the property yields no mixed prime orientation (PRCCharacterNoMixedPrimeOrientation_of_reciprocal_witness_globalizes) and forces the distinguished two-orbit to be reciprocal whenever any prime is (PRCCharacterPrimeReciprocalForcesTwoPrimeReciprocal_of_reciprocal_witness_globalizes). It is equivalent to a split packaging that separates the two-prime force from the remaining primes, and it is recovered from local orientation plus no-mixing.
The blocker certificate for native-cost uniqueness consumes this interface. In the broader RS chain, unique native cost feeds the J-cost uniqueness step (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law; without a cross-prime orientation law, characters could mix reciprocal and identity axes and spoil uniqueness of the cost pulled back from the character. The companion identity-orientation globalization is the dual missing relation noted in the module comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.