PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_admissible
plain-language theorem explainer
For any admissible ratio character, fixing a native prime axis is equivalent to fixing the distinguished orbit-2 axis. Cost-uniqueness and orientation-coherence arguments cite this normal form. The proof combines the one-sided forcing lemma with a reciprocal-twist contradiction that rules out mixed orientations.
Claim. Let $\chi$ be a map on ratio orbits that is an admissible ratio character (ratio-character laws, prime calibration, and prime-pair product cost consistency). Then for every prime orbit $p$, $\chi$ fixes the prime direction of $p$ under cross-equality if and only if $\chi$ fixes the distinguished two-prime direction under cross-equality.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed numerator orbits over nonzero distinction-nat denominators. Cross-equality crossEq is the internal rational relation: two orbits match when scaled numerators balance under cross-multiplication. The reciprocal of a ratio orbit is total (zero maps to zero).
A ratio character $\chi$ acts on these orbits. Admissibility (repaired after the two-adic countermodel) requires the ratio-character laws, prime-direction calibration, and prime-pair product cost consistency. That package keeps the two global orientations and excludes valuation twists.
The target property is the identity-iff-two normal form: identity orientation on any native prime axis is equivalent to identity orientation on the distinguished orbit-2 prime axis. The one-sided forcing half (prime identity implies two-identity) is already available under prime-pair product cost consistency; the converse is recovered via the reciprocal twist.
proof idea
First obtain the one-sided forcing statement from the prime-pair product cost consistency package on the admissible character. For each prime $p$, the forward implication is that forcing lemma.
For the reverse: assume $\chi$ fixes the two-prime direction. Local prime calibration yields that $\chi$ either fixes the $p$-direction or sends it to its reciprocal. The identity case is immediate. In the reciprocal case, form the reciprocal twist of $\chi$ (still admissible). Forcing on the twist plus the twist identity-at-$p$ gives that the twist fixes the two-direction, which unwinds to $\chi$ sending two to its reciprocal. Transitivity with the assumed two-identity then yields that the two-direction is cross-equal to its own reciprocal, contradicting that a prime orbit direction is never cross-equal to its reciprocal.
why it matters
This closes the two-sided normal form for prime orientations under the repaired admissible-character interface. The immediate consumer is PRCCharacterPrimeOrientationCoherent_of_admissible, which packages local orientation coherence for every calibrated prime once identity-iff-two is in hand.
In the broader Recognition stack this sits inside native cost uniqueness for PRC characters: admissible characters cannot mix identity and reciprocal orientations across prime axes without breaking cost consistency. That coherence is a prerequisite for identifying the native cost with the unique $J$-cost forced by the Recognition Composition Law (T5 in the forcing chain), before $\phi$ and the eight-tick structure are imposed downstream.
No scaffolding remains on this declaration; it is a proved bridge from admissibility to orientation coherence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.