PRCCharacterPrimeIdentityForcesTwoPrimeIdentity_of_identity_iff_two
plain-language theorem explainer
If a ratio-orbit character obeys the identity-iff-two normal form on native prime axes, then identity orientation at any calibrated prime forces identity at the distinguished orbit-2 axis. Native-cost uniqueness certificates and the prime-calibration target ladder cite this reduction. Proof is a one-line extraction of the forward half of the given biconditional.
Claim. Let $\chi$ be a map on ratio orbits. Suppose that for every native prime axis $p$, identity orientation of $\chi$ at $p$ is equivalent to identity orientation of $\chi$ at the distinguished orbit-$2$ prime axis. Then identity orientation of $\chi$ at any native prime axis forces identity orientation of $\chi$ at the orbit-$2$ axis.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters are maps $\chi$ on ratio orbits; orientation of $\chi$ relative to a direction is recorded by cross-equality of orbits.
Native primes supply calibrated axes via prime directions. The distinguished orbit-2 prime axis is the reference for both normal forms used here. The identity-iff-two form says $\chi$ is identity-oriented on a native prime axis exactly when it is identity-oriented on the orbit-2 axis. The one-sided form keeps only the forward implication: identity at any calibrated prime forces identity at orbit 2. (The reverse is recovered at target level by applying the same statement to the reciprocal twist of the character.)
This module develops uniqueness of the native cost built from such characters, in support of the Recognition Composition Law and the J-uniqueness step of the forcing chain.
proof idea
One-line wrapper extracting the forward direction of a biconditional. Introduce a native prime $p$, its primality witness, and the assumption that $\chi$ is identity-oriented at the prime direction of $p$. Apply the left-to-right half of the given identity-iff-two hypothesis at that prime to conclude identity orientation at the orbit-2 axis.
why it matters
Sits in the normal-form ladder for native-cost uniqueness. Downstream, the prime-calibration target theorem of the same shape applies this result to characters satisfying the calibrated iff form, yielding the one-sided target. The implication is packaged into the native-cost uniqueness blocker certificate and appears in the conditional universal-foundation certificate.
In the Recognition framework this controls how admissible characters may orient on prime axes relative to the orbit-2 reference, supporting uniqueness of the native cost that realizes the J-cost $J(x)=(x+x^{-1})/2-1$ forced at T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.