PRCCharacterNonunitIdentityWitnessReflectsPrimeWitness_of_prime_local
plain-language theorem explainer
If a ratio character is product-display compatible and locally orients every prime axis to itself or its reciprocal, then identity orientation on any non-unit orbit forces identity on at least one prime axis. Cost-uniqueness and trace-transport arguments cite this to rule out “all primes inverted, yet some composite fixed.” The proof is contradiction: all-prime reciprocal lifts to the given non-unit, then cross-equivalence yields direction equals reciprocal, which non-units forbid.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal under cross-equivalence), compatible with native orbit-product display, and such that every prime axis is sent either to itself or to its reciprocal. If $p$ is a nonzero non-unit distinction number whose orbit direction is fixed by $\chi$ (identity orientation), then there exists a prime $q$ whose prime direction is likewise fixed by $\chi$.
background
Primitive Recognition Calculus works with distinction numbers and ratio orbits: a ratio orbit is a signed-orbit numerator over a nonzero distinction denominator. Equality of displays is the internal cross-multiplication relation crossEq (balanced scaled numerators), not definitional equality, so characters and orientations stay quotient-native.
A ratio character $\chi$ preserves the unit orbit, multiplies under orbit product, and intertwines reciprocal, all up to crossEq. Product-display compatibility is the extra quotient-respect step: $\chi$ on a composite orbit direction agrees with $\chi$ on the product of the factor directions. Local prime orientation says each prime axis is sent to itself or to its reciprocal; that is the algebraic content of matching $J$-cost on a single prime direction.
Identity orientation on an arbitrary nonzero orbit means $\chi$ fixes that direction under crossEq. Reciprocal orientation means it sends the direction to its reciprocal. The reciprocal map on ratio orbits is total (zero to zero), and crossEq is symmetric and transitive via the integer bridge.
proof idea
Argue by contradiction: assume no prime has identity orientation. Local prime orientation then forces every prime axis into reciprocal orientation.
Apply the upstream lift that product-display-compatible characters sending all primes to reciprocal send every non-unit orbit direction to reciprocal. Specialize to the given non-unit $p$ to obtain reciprocal orientation on $p$.
Identity on $p$ plus reciprocal on $p$, with crossEq symmetry and transitivity, yields that the orbit direction of $p$ is cross-equivalent to its own reciprocal. The non-unit lemma that no non-unit orbit direction is cross-equivalent to its reciprocal closes the contradiction.
why it matters
Native cost uniqueness for PRC needs characters that cannot mix “composite fixed” with “all primes inverted.” This lemma converts a single non-unit identity witness into a prime identity witness under local prime orientation and product-display compatibility.
Downstream, it feeds the comparable-trace respect theorem for non-unit identity and the globalization of prime-identity witnesses into successor transport on prime-floor orbits. Those steps sit in the uniqueness pipeline that ties ratio characters to doubled-trace d'Alembert data and ultimately to the forced $J$-cost shape (T5: $J(x)=(x+x^{-1})/2-1$) in the forcing chain.
Without this reflection, a character could fix a composite while inverting every prime axis, breaking coherent trace transport and blocking uniqueness of the native cost factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.