PRCCharacterPrimeReciprocalWitnessGlobalizesSplit
plain-language theorem explainer
The split form of reciprocal-witness globalization for a ratio-orbit character decomposes the property into two directed axis rules: any calibrated prime reciprocal forces the orbit-2 reciprocal, and the orbit-2 reciprocal forces every prime reciprocal. Native-cost uniqueness arguments cite this when they reason along the distinguished 2-axis separately from the all-primes direction. It is the definitional conjunction of those two forcing predicates.
Claim. For a map $\chi$ on rational ratio orbits, the split reciprocal-witness globalization property holds when (i) reciprocal orientation of $\chi$ at any calibrated prime axis forces reciprocal orientation at the orbit-$2$ prime axis, and (ii) reciprocal orientation at the orbit-$2$ prime axis forces reciprocal orientation at every calibrated prime axis.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator. Characters are self-maps $\chi$ of ratio orbits used to read cost orientation. Reciprocal orientation means $\chi$ agrees, under cross-equality of orbits, with the reciprocal automorphism on a given prime direction (the reciprocal event swaps source and target and inverts the ratio).
Native cost uniqueness work forces characters that match the J-cost on doubled traces. Reciprocal-witness globalization says that a single calibrated prime where $\chi$ acts as reciprocal already forces the reciprocal branch on the whole prime lattice. The split form isolates the distinguished orbit-$2$ axis as an intermediate station.
Upstream, the first conjunct is the converse distinguished-axis rule: reciprocal orientation at any calibrated prime forces reciprocal orientation at orbit $2$. The second is the two-to-all reciprocal rule. The upstream doc states that together they are "exactly reciprocal-witness globalization."
proof idea
Definitional abbreviation only. The body is the conjunction of the two already-defined directed forcing predicates (prime-to-two and two-to-all). No tactics, no lemmas applied at this site; obligations live in the conversion theorems that relate the split form to the monolithic globalization statement.
why it matters
Feeds the equivalence between monolithic reciprocal-witness globalization and this split form, plus the two conversion theorems in both directions. The of-split direction is a short composition: apply prime-to-two, then two-to-all. The reverse packages a global witness into the pair of directed rules.
The native-cost uniqueness blocker certificate and the universal-foundation open-target ledger both carry this interface among the exact Lean targets that isolate missing mathematics: uniqueness is not closed, but the reciprocal-branch transport is factored into checkable pieces. In the broader forcing chain this sits under J-uniqueness (T5) and the Recognition Composition Law infrastructure for native cost characters; it does not itself finish uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.