PRCCharacterZero_of_prime_orientation_coherent
plain-language theorem explainer
A ratio-orbit character with coherent prime-axis orientation must send the zero orbit to zero under cross-equivalence. Anyone proving uniqueness of the native PRC cost factorization cites this to pin the character at the origin. The argument multiplies zero by the two-prime direction, cancels in the rational display, and rules out the residual case that would force the two-direction to the unit.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal under cross-equivalence). If $\chi$ is prime-orientation coherent—either $\chi$ fixes every native prime direction or $\chi$ sends every native prime direction to its reciprocal—then $\chi(0)\sim 0$ under cross-multiplication equivalence of ratio orbits.
background
In the Primitive Recognition Calculus, costs factor in d'Alembert form through ratio-orbit characters. A PRCRatioCharacter is a map $\chi$ on ratio orbits that preserves the unit, multiplies under the orbit product, and respects reciprocals, all up to cross-equivalence rather than definitional equality, so the statements stay quotient-native.
Cross-equivalence (crossEq) is the internal PRC rational relation: two orbits match when cross-multiplication of numerators and denominators balances as signed orbits. It agrees with equality of the rational verifier displays (crossEq_iff_toRat_eq).
Prime-orientation coherence means the character chooses one global policy on every native prime direction: either the identity on all of them, or the reciprocal on all of them. The two-prime direction is the concrete test axis used here; its rational display is $2$, so it cannot be cross-equivalent to the unit orbit.
proof idea
First obtain that $\chi$ respects cross-equivalence from the canonical normalize-ratio target. Show $\chi$ of the two-prime direction is not cross-equivalent to one: coherence gives either identity or reciprocal on that prime, and either case plus $\chi(\mathrm{two})\sim 1$ forces $2=1$ or $1/2=1$ in the rational display (norm_num).
Zero times the two-direction is cross-equivalent to zero. Respect of crossEq and multiplicativity then yield $\chi(0)\sim\chi(0)\cdot\chi(\mathrm{two})$. Pass to rationals. If $\chi(0).\mathrm{toRat}=0$, done. Otherwise left-cancel to force $\chi(\mathrm{two}).\mathrm{toRat}=1$, contradicting the earlier non-unit claim.
why it matters
Native cost uniqueness in PRC needs characters that arise from coherent prime orientation to match the global target factorization. This lemma supplies the missing zero-point: without $\chi(0)\sim 0$, the multiplicative character could drift off the cost ladder at the origin.
It is consumed by PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget_proved, which lifts signed coherent prime orientation to the full global target. That step sits inside the native-cost uniqueness development for the d'Alembert factorization of PRC costs, the same uniqueness chain that feeds J-cost identification (T5: $J(x)=(x+x^{-1})/2-1$) once the character is pinned.
No scaffolding remains here: the claim is fully proved and closes one local obligation on the path from prime-axis coherence to global character rigidity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.