PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget
plain-language theorem explainer
Packages the Prop that every prime-calibrated ratio character with reciprocal orientation on any native prime axis must put the orbit-2 prime axis on the reciprocal branch. Native-cost uniqueness certificates, branch-equivalence lemmas, and the UniversalFoundation open-target list cite this name. Pure Prop abbreviation: no proof content, only a quantified interface over characters.
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 matches canonical $J$-cost on each prime orbit), the following holds: if $\chi$ is reciprocal on any native prime axis, then $\chi$ is reciprocal on the orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed numerator over a nonzero distinction-nat denominator. A ratio character $\chi$ is a map on these orbits; the generated cost is compared to the canonical $J$-cost (the unique cost forced by the Recognition Composition Law and T5) via cross-equality of orbits.
Prime-direction calibration means that on every native prime orbit the character-generated cost agrees with canonical $J$ on that prime direction. Reciprocal orientation means $\chi$ sends a prime direction to its reciprocal orbit (the inverse-ratio branch), matching the reciprocal automorphism of the cost algebra and the reciprocal recognition event in ledger forcing.
The packaged property is the converse distinguished-axis reciprocal normal form: reciprocal orientation at any calibrated prime forces reciprocal orientation at the distinguished orbit-$2$ prime axis. Together with the two-to-all reciprocal rule, that is exactly reciprocal-witness globalization.
proof idea
Definitional Prop packaging only. The body is the universal quantification: for all $\chi$, if $\chi$ is a ratio character and prime-direction calibrated, then the already-named predicate "prime-reciprocal forces two-prime-reciprocal" holds of $\chi$. No tactics, no lemmas applied at this site; downstream theorems discharge or refute the packaged target by introducing $\chi$ and applying character-level lemmas.
why it matters
This is one exact Lean target into which Pass-25 splits the still-open native cost uniqueness problem (see the blocker certificate). It is the reciprocal-branch half of the distinguished-axis converse; an iff theorem equates it with the parallel identity-branch target, and a one-line transport derives each from the other.
It is implied by full reciprocal-witness globalization, and it appears among the UniversalFoundation open targets. Framework-wise it sits under T5 $J$-uniqueness and the RCL: native cost uniqueness needs every admissible character to land on the canonical $J$ branch structure (identity vs reciprocal) consistently across prime axes, with orbit-$2$ as the distinguished generator of the eight-tick octave (T7).
Importantly, the target as stated has been refuted in-module: the packaged Prop is false, so uniqueness cannot route through this exact converse form and must use a refined split (witness globalization / other blockers).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.