PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesSplitTarget
plain-language theorem explainer
Packages reciprocal globalization as the conjunction of two directional targets: any reciprocal native prime forces the orbit-2 prime reciprocal, and orbit-2 reciprocal forces every native prime reciprocal. Cited by the native-cost uniqueness blocker certificate and the split/globalize iff chain. Pure definitional conjunction of the two already-named Prop targets.
Claim. The split reciprocal-globalization target is the conjunction of: (i) for every ratio character $\chi$ that is prime-direction calibrated, if some native prime axis is reciprocal then the orbit-$2$ prime axis is reciprocal; and (ii) for every such calibrated $\chi$, if the orbit-$2$ prime axis is reciprocal then every native prime axis is reciprocal.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode how recognition cost orients along prime axes. Prime-direction calibration pins the distinguished (identity-linked) orientation so that cost minima sit at the identity event $x=1$. A prime axis is on the reciprocal branch when the character sends that prime orbit to its reciprocal rather than its direct image.
The two conjuncts isolate transport through the orbit-$2$ axis. The first says any reciprocal native prime forces orbit-$2$ onto the reciprocal branch; the second says orbit-$2$ reciprocal forces every native prime reciprocal. Together they are the split form of full reciprocal witness globalization under prime calibration.
Local module setting is native-cost uniqueness: which cost functionals arise from calibrated characters, and which orientation hypotheses close the uniqueness argument.
proof idea
Definitional packaging only. The body is the conjunction of PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget and PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget. No tactics, no lemmas applied at this site.
why it matters
Exact remaining split of the reciprocal-globalization obligation inside native-cost uniqueness. Downstream, the blocker certificate records that uniqueness is not closed and lists this (and related) targets as the missing mathematics. Iff theorems equate the unsplit globalization target with this split form, and equate the split form with the two-to-all half alone once exclusion lemmas are in place.
A later theorem refutes the split target outright, so the reciprocal-globalization route via prime calibration is closed negatively: identity orientation does not propagate across prime axes in the hoped-for way. That refutation feeds the Pass-25 certificate structure and forces the uniqueness program onto other factorization or signed-admissible routes rather than this reciprocal-witness path. Framework-wise it sits under J-cost uniqueness and character calibration (T5-adjacent native cost), not under the geometric T7/T8 steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.