PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_identity_forces_two
plain-language theorem explainer
If prime calibration forces identity on the orbit-2 axis whenever any calibrated prime axis is identity, then it also forces every native prime axis onto the reciprocal branch once orbit-2 is reciprocal. Native-cost uniqueness and the reciprocal-globalization half of the PRC calibration program cite this implication. The proof is a two-step term composition through the intermediate two-reciprocal-excludes-identity target.
Claim. Assume that for every ratio-orbit character that is prime-direction calibrated, identity on any calibrated prime axis forces identity on the orbit-$2$ prime axis. Then, for every such character, if the orbit-$2$ prime axis lies on the reciprocal branch, every native prime axis lies on the reciprocal branch.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding the signed branch (identity versus reciprocal) of the native cost along each prime axis. Prime-direction calibration restricts how $\chi$ may assign those branches on the distinguished prime axes that generate the native factorization.
Two one-sided globalization targets appear. The identity target says: if any calibrated prime axis sits on identity, then the orbit-$2$ axis must sit on identity. The reciprocal target says the dual: once orbit-$2$ is reciprocal, every native prime axis is reciprocal. Both are packaged as universal statements over calibrated ratio characters.
An intermediate exclusion target sits between them: if orbit-$2$ is reciprocal, then no native prime axis may remain on identity. Upstream lemmas already convert the identity-forces-two hypothesis into that exclusion target, and convert exclusion into full reciprocal globalization.
proof idea
Pure term composition of two already-proved bridges. First apply PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_of_identity_forces_two to the given identity-forces-two hypothesis, obtaining the two-reciprocal-excludes-identity target. Feed that into PRCPrimeCalibrationForcesTwoPrimeReciprocalForcesPrimeReciprocalTarget_of_two_prime_reciprocal_excludes, which upgrades exclusion of residual identity axes into the full reciprocal-forces-reciprocal target. No new character-level reasoning occurs here.
why it matters
Closes one direction of the equivalence between the identity-side and reciprocal-side distinguished-axis targets (..._iff_identity_forces_two). That equivalence is part of the native-cost uniqueness blocker certificate and is consumed by the conditional universal-foundation certificate in UniversalFoundation. In the broader RS forcing picture this is bookkeeping on the J-cost branch structure (T5 uniqueness of $J$), not a new physical constant: it ensures calibrated prime axes cannot mix identity and reciprocal branches once the orbit-$2$ axis is fixed, which is required before the native cost can be identified with the unique d'Alembert solution $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.