PRCPrimeCalibrationPropagationTarget_of_sharpened_orientation
plain-language theorem explainer
Once a sharpened orientation package is assumed, prime-calibrated ratio characters match native cost on every rational orbit. Citation target for the unique-factorization half of native-cost rigidity in the Primitive Recognition Calculus. The argument is a pure nested term: local orientation and no-mix force coherent prime orientation, which with the global-propagation conjunct yields the classical propagation target via an intermediate global-orientation lemma.
Claim. Assume the sharpened prime-calibration package: prime-floor successor transport holds in sharpened form, and coherent prime orientation propagates to a global orientation. Then every ratio character $\chi$ calibrated on all prime directions has character cost cross-equal to the native cost on every rational orbit $q$.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding a candidate cost law. Prime-direction calibration means $\chi$ already matches the native cost on every prime orbit. The propagation target asks that this match extend to every rational orbit: the unique-factorization side of native-cost rigidity ("sharper target B" in the module).
The sharpened package (Pass-27) is the conjunction of a refined prime-floor successor transport hypothesis and the claim that coherent prime orientation already propagates to a global orientation. Upstream work forces local prime orientation unconditionally, rules out mixed orientations once prime-identity traces cohere, and assembles coherent orientation from those two pieces.
Global orientation is then obtained by feeding coherent orientation into the second sharpened conjunct. A separate wrapper turns global orientation into full propagation to every rational orbit.
proof idea
Pure nested term application, no tactics. From the first conjunct of the sharpened hypothesis one obtains prime-floor successor transport, then comparable-trace, common-trace-extension, trace-transport, and finally prime-identity trace coherence. Trace coherence yields the no-mixed-orientation target. The already-proved local orientation lemma plus no-mix give coherent prime orientation. The second sharpened conjunct upgrades coherent orientation to global orientation. The final step applies the existing wrapper from global orientation to the classical propagation target.
why it matters
This bridge is the reduction step used to refute the sharpened package itself: if the sharpened target held, propagation would hold, but propagation is already refuted, so the sharpened target fails. That refutation feeds the native-cost uniqueness blocker certificate, which records which factorization routes are closed.
In framework terms the lemma sits on the unique-factorization side of cost rigidity, the companion to J-uniqueness (T5) and the Recognition Composition Law. It does not itself force the cost functional; it only shows that a particular strengthened orientation route would have implied full prime-to-rational propagation, and thereby helps close that route in the uniqueness ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.