PRCCharacterPrimeIdentityForcesTwoPrimeIdentity
plain-language theorem explainer
Defines the one-sided orientation constraint on a ratio-orbit character: if any calibrated prime axis is identity-oriented under χ, then the distinguished orbit-2 prime axis must also be identity-oriented. Downstream uniqueness and orientation lemmas cite this Prop as the normal form that identity at primes forces identity at 2. The body is a pure universal implication over prime orbits and cross-equality; no proof content.
Claim. For a map $\chi$ on ratio orbits, the following holds: whenever $p$ is a prime distinction-orbit and $\chi$ fixes the corresponding prime direction up to cross-multiplication equality, then $\chi$ also fixes the distinguished prime direction of orbit $2$ up to the same equality.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction-orbit denominator. Two such displays are identified by cross-multiplication equality (crossEq): the scaled numerators balance as signed orbits, which is the internal PRC stand-in for rational equality.
A character $\chi$ is a self-map of ratio orbits. Prime axes are the calibrated directions attached to prime distinction-orbits (primeDirection); among them, the orbit-$2$ prime axis (twoPrimeDirection) is distinguished. Identity orientation at an axis means $\chi$ sends that direction to a cross-equal copy of itself (the character acts as the identity on that ray).
The reciprocal automorphism and reciprocal events supply the dual orientation (swap source/target and invert the ratio). The module develops native cost uniqueness by constraining how characters may orient prime axes relative to the doubled-trace / d'Alembert cost structure.
proof idea
Pure definitional expansion: the Prop is the universal statement that for every prime distinction-orbit $p$, cross-equality of $\chi$ on the $p$-prime direction with that direction itself implies the same cross-equality on the orbit-$2$ prime direction. No tactics or lemmas; downstream theorems discharge or relate instances of this Prop.
why it matters
This is the one-sided normal form used throughout native cost uniqueness: identity at any calibrated prime forces identity at the orbit-$2$ axis. Downstream results include the iff with the contrapositive exclusion form (reciprocal orientation at $2$ excludes identity at any prime), the witness variant, derivation from the two-sided iff, from local two-prime reciprocal exclusion, from prime-pair product cost consistency, and from the reciprocal-twist of the dual reciprocal-forces-two statement.
In the Recognition forcing picture this pins character orientation on the prime lattice before J-cost uniqueness (T5) and the self-similar fixed point $\phi$ (T6) are read off the native cost. The reverse direction is recovered by applying the same form to the reciprocal twist of $\chi$, so the full two-sided control sits one twist away.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.