PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_of_two_prime_branch_controls
plain-language theorem explainer
Under prime-direction calibration, if the orbit-2 branch controls every native prime branch, then identity orientation on any prime axis is equivalent to identity on the orbit-2 axis. Cited by the native-cost uniqueness blocker certificate and the two-target equivalence. Proof applies the character-level identity-iff-two lemma to the already-proved local orientation target plus the assumed branch-control hypothesis.
Claim. Assume that every prime-direction-calibrated ratio character has the property that the branch chosen at orbit $2$ controls every native prime branch. Then every such character satisfies: identity orientation holds on an arbitrary prime axis if and only if it holds on the distinguished orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode orientation data along prime directions. Prime-direction calibration restricts $\chi$ so that its action on each prime axis is a calibrated choice of branch. Two distinguished targets package what calibration is required to force:
- Branch-control target: the branch chosen at the orbit-$2$ prime axis controls every native prime branch.
- Identity-iff-two target: identity orientation on any prime axis holds exactly when identity holds on the orbit-$2$ axis.
Upstream, local prime orientation under calibration is already proved unconditionally (PRCPrimeCalibrationForcesLocalPrimeOrientationTarget_proved). At character level, local orientation plus two-prime branch control yields the identity-iff-two property (PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_local_two_prime_branch_controls). This declaration lifts that character lemma to the calibration-target layer.
proof idea
Term-mode, three-line argument. Introduce a calibrated ratio character $\chi$. Feed it to the already-proved local-orientation target to obtain local prime orientation, and to the assumed branch-control target hypothesis to obtain two-prime branch control. Apply the character-level lemma PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_local_two_prime_branch_controls to those two facts; the conclusion is exactly the identity-iff-two target for $\chi$.
why it matters
Closes one direction of the equivalence between the branch-control target and the identity-iff-two target (PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_iff_prime_identity_iff_two). That equivalence is part of the native-cost uniqueness blocker certificate, which packages the remaining obstructions to uniqueness of the native cost functional built from ratio characters and doubled traces. Downstream it also feeds the conditional universal-foundation certificate. In the broader RS forcing picture this sits inside the uniqueness route for the J-cost (T5), where calibrated prime orientations must collapse to a single coherent choice before the Recognition Composition Law can pin $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.