PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_of_identity_forces_two
plain-language theorem explainer
If prime calibration already forces identity on the orbit-2 axis whenever any calibrated prime axis is identity, then identity on an arbitrary prime axis is equivalent to identity on orbit 2. Cited by the native-cost uniqueness blocker path and the coherent prime-orientation target. Proof is a short case split on local orientation, using reciprocal twist of the character to derive a contradiction on the two-axis.
Claim. Assume that every ratio-orbit character that is prime-direction calibrated, and that sits on the identity branch at some prime axis $p$, must also sit on the identity branch at the distinguished prime axis $2$. Then, for every such character and every prime $p$, the character is identity-oriented at $p$ if and only if it is identity-oriented at $2$.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit displays (signed numerator over a nonzero distinction-nat denominator). Equality of displays is the internal cross-multiplication relation crossEq, which is symmetric and transitive and matches rational equality of verifier displays. Reciprocals of ratio orbits are total, sending zero to zero.
A PRC ratio character $\chi$ assigns to each ratio orbit another ratio orbit. Prime-direction calibration constrains how $\chi$ acts on prime axes. Each prime axis has a local orientation that is either the identity branch or the reciprocal branch. The distinguished two-step orbit (the prime axis $2$) plays a special role in later cost uniqueness arguments.
The one-sided target says calibration plus identity at any prime forces identity at $2$. The two-sided target strengthens this to an equivalence: identity at a prime holds exactly when identity at $2$ holds. This lemma discharges the reverse implication under the one-sided hypothesis.
proof idea
Fix a calibrated character $\chi$ and a prime $p$. The forward direction (identity at $p$ implies identity at $2$) is exactly the one-sided hypothesis.
For the converse, assume identity at $2$. Local prime orientation at $p$ is either identity or reciprocal. The identity case is immediate. In the reciprocal case, form the reciprocal twist of $\chi$. The twist turns the reciprocal orientation at $p$ into an identity orientation, so the one-sided hypothesis applied to the twist yields identity at $2$ for the twisted character. Unwinding the twist converts that into a reciprocal orientation of the original $\chi$ at $2$. Transitivity of crossEq with the assumed identity at $2$ then forces the two-axis to be cross-equal to its own reciprocal, contradicting the prime-direction non-self-reciprocal lemma on the two-orbit.
why it matters
This is the hard half of the equivalence between the one-sided distinguished-axis target and the identity-iff-two target. The sibling biconditional packages both directions and feeds the two-prime branch-control ladder that produces coherent prime orientation from prime-pair product cost consistency.
Downstream, coherent orientation is part of the native-cost uniqueness blocker certificate and appears in the conditional universal-foundation certificate. In the Recognition forcing chain this sits in the foundation layer that pins the native cost character before J-uniqueness (T5) and the self-similar fixed point $\phi$ (T6) are invoked at the physics interface. Closing the iff removes a free orientation choice that would otherwise obstruct uniqueness of the native cost on prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.