PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_of_identity_forces_two
plain-language theorem explainer
If prime calibration forces identity at the orbit-2 axis whenever any calibrated prime axis is identity-oriented, then it also forces two-reciprocal exclusion: orbit-2 reciprocal orientation rules out identity on every native prime axis. Native-cost uniqueness certificates and the target-equivalence lemma cite this lift. Proof is a one-line unpack of the universal target Prop, then the character-level implication.
Claim. Assume every ratio-orbit character that is a PRC ratio character and prime-direction calibrated satisfies: identity orientation at any calibrated prime axis forces identity orientation at the orbit-$2$ prime axis. Then every such character also satisfies: if the orbit-$2$ prime axis is reciprocal-oriented, no native prime axis remains identity-oriented.
background
In the Primitive Recognition Calculus, ratio-orbit characters assign to each ratio orbit either an identity or reciprocal orientation. Prime-direction calibration restricts how those orientations sit on native prime axes. Two target Props package the global forcing statements one wants for every calibrated character.
The one-sided distinguished-axis target says prime calibration must force identity at the orbit-$2$ prime axis from identity at any calibrated prime axis. The two-reciprocal exclusion target says the opposite branch: if calibration leaves orbit-$2$ on the reciprocal branch, no native prime axis may remain on identity.
At character level, the upstream lemma already shows the local implication: any character that satisfies identity-forces-two-identity also satisfies two-reciprocal-excludes-prime-identity (by contraposing the forced identity at orbit-$2$). This declaration lifts that character fact to the quantified target Props used by the uniqueness certificates.
proof idea
One-line wrapper. Unpack the conclusion target by introducing a character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the assumed identity-forces-two target at $(\chi,h\chi,h\mathrm{prime})$ to obtain the character-level hypothesis. Discharge with the upstream character lemma PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentity_of_identity_forces_two, which turns that hypothesis into two-reciprocal exclusion for $\chi$.
why it matters
This is one direction of the equivalence between the two prime-calibration targets (identity-forces-two versus two-reciprocal-excludes). Downstream, that equivalence and this lift feed the witness-target and forces-prime-reciprocal-target variants, and appear in the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate.
In the Recognition framework the native-cost uniqueness program is the PRC-side route to J-uniqueness (forcing-chain T5): only the reciprocal-symmetric cost survives calibrated prime-axis constraints. Closing the identity-versus-reciprocal branch analysis at orbit-$2$ is a necessary step before the cost functional is forced to the unique $J(x)=(x+x^{-1})/2-1$ shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.