PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget
plain-language theorem explainer
Packages the open target that every prime-calibrated ratio character must globalize reciprocal orientation: one reciprocal native-prime witness forces reciprocal orientation on every native prime axis. Native-cost uniqueness work cites it as the reciprocal-globalization half of the prime-calibration program. The body is a bare Prop abbreviation, not a proof.
Claim. For every map $\chi$ from ratio orbits to ratio orbits that is a ratio character and is calibrated on every native prime direction (its generated cost agrees with canonical $J$-cost on each prime orbit), reciprocal-witness globalization holds for $\chi$: if prime calibration admits one reciprocal-oriented native prime witness, then reciprocal orientation holds on every native prime axis.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays (signed numerator over a nonzero distinction-orbit denominator). A ratio character $\chi$ is a map on those orbits; the associated cost is built from $\chi$ and compared to the canonical $J$-cost on ratio orbits.
Prime-direction calibration means that for every prime orbit $p$, the cost generated by $\chi$ on the prime direction agrees with the canonical on-orbit $J$-value (cross-equality of ratio orbits). Reciprocal orientation is the branch that sends a direction to its inverse-ratio partner, matching the reciprocal automorphism of the cost algebra and the reciprocal recognition event (source/target swap with inverted ratio).
This module isolates exact Lean targets for native cost uniqueness. The present definition is the globalization target: calibration plus one reciprocal prime witness should force the reciprocal branch on all native primes, ruling out mixed prime orientations.
proof idea
Definitional Prop package only. The body is the universal quantification over maps $\chi$: assume ratio-character and prime-direction calibration, conclude the reciprocal-witness globalization predicate on $\chi$. No tactics, no lemmas applied, no proof obligation discharged.
why it matters
Sits inside the native-cost uniqueness blocker stack. Downstream, assuming this target yields the no-mixed-prime-orientation target, the two-prime reciprocal force target, and the split globalization target; it is also iff-equivalent to no-mixed orientation and to the identity-witness-excludes-reciprocal target. The pass-25 blocker certificate records that uniqueness is not closed and splits the missing mathematics into exact targets of this shape.
In the broader Recognition forcing chain this is infrastructure toward $J$-uniqueness (T5): characters calibrated on primes must not mix identity and reciprocal branches if the cost is to match the unique $J(x)=(x+x^{-1})/2-1$ solving the Recognition Composition Law. Closing the target would remove one mixed-orientation obstruction on the path from prime calibration to a unique native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.