PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_iff_split
plain-language theorem explainer
Prime-calibration reciprocal-witness globalization is equivalent to its two-step split: transport any reciprocal prime witness onto the orbit-2 axis, then from orbit-2 onto every native prime axis. Cost-uniqueness and universal-foundation certificates cite this bridge when packaging the reciprocal half of native-cost uniqueness. The proof is a pure Iff constructor from the two already-proved one-way implications.
Claim. The following are equivalent. (A) For every ratio-orbit character that is prime-direction calibrated, a single reciprocal-oriented native prime witness forces reciprocal orientation on every native prime axis. (B) Prime calibration forces both (i) reciprocal transport from an arbitrary native prime axis onto the orbit-$2$ prime axis and (ii) reciprocal transport from the orbit-$2$ axis onto every native prime axis.
background
In the Primitive Recognition Calculus, ratio-orbit characters $\chi$ assign oriented multiplicative data along native prime axes. Prime-direction calibration fixes how $\chi$ treats those axes relative to the distinguished orbit-$2$ direction. A reciprocal witness on one prime axis means $\chi$ sits on the reciprocal branch there rather than the identity branch.
The unsplit target asserts that, under prime calibration, one such reciprocal witness globalizes: every native prime axis must then be reciprocal. The split target factors that claim into two transport steps: arbitrary prime $\to$ orbit-$2$, then orbit-$2$ $\to$ all primes. Both halves are named propositions in the same uniqueness module; this declaration only equates the packaged forms.
The surrounding development aims at native-cost uniqueness for the Recognition $J$-cost (the unique continuous solution of the Recognition Composition Law with $J(1)=0$, $J(x)=J(x^{-1})$), via character-trace matching and d'Alembert-type identities on doubled traces.
proof idea
Term-mode Iff introduction. The forward arrow applies the already-proved lemma that any global reciprocal-witness target yields both split conjuncts (prime-to-two and two-to-all). The reverse arrow applies the lemma that reconstructs full globalization from the split pair, by introducing a calibrated character and invoking the split-form witness globalization on that character. No new arithmetic is done here.
why it matters
Native-cost uniqueness needs reciprocal orientation to propagate once it appears on any calibrated prime axis; otherwise signed or mixed-branch characters could spoil uniqueness of the cost reconstructed from the character. Packaging the unsplit target as equivalent to the two-step split lets later certificates discharge globalization piecewise.
Downstream, prc_native_cost_uniqueness_blocker_certificate records proved and refuted factorization targets that close the uniqueness blocker, and prc_universal_foundation_conditional_certificate assembles kernel, real-complete ordered field, and trace-logic passes into the conditional universal foundation. This iff is bookkeeping on the reciprocal half of that chain, not a new physical law, but it is the clean interface between the global statement and the prime-to-two / two-to-all lemmas used in the forcing path toward unique $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.