PRCCharacterMixedNonunitIdentityWitnessReflectsPrimeWitness_of_prime_local
plain-language theorem explainer
Under local prime orientation, a ratio character that is product-display compatible cannot keep a mixed nonunit pair (identity on one nonunit axis, reciprocal on another) without also fixing some prime axis to the identity. Cost-uniqueness and prime-calibration arguments cite this reflection law. The proof is by contradiction: all-prime-reciprocal forces every nonunit reciprocal, so an identity nonunit collapses to a self-reciprocal direction, which is impossible.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal under cross-equivalence). Suppose $\chi$ respects native orbit-product displays, and on every prime axis $\chi$ is cross-equivalent either to the axis itself or to its reciprocal. Then: if there exist nonunit directions with both identity and reciprocal character values, some prime axis must be identity-oriented under $\chi$.
background
Primitive Recognition Calculus works with ratio orbits: integer-numerator / nonzero-denominator displays of distinction orbits, compared by cross-equivalence (balanced cross-multiplication of signed orbits) rather than definitional equality. Reciprocals and products are total operations on these displays.
A ratio character $\chi$ is a map on ratio orbits that fixes the unit, multiplies under the orbit product, and sends reciprocals to reciprocals, all up to cross-equivalence. Product-display compatibility is the extra quotient-respect step: the character on a composite orbit agrees with the character of the product of the factor orbits. Prime-local orientation says each prime axis is sent either to itself or to its reciprocal; that is the algebraic content of equal $J$-cost on a single prime direction.
The target property is the identity half of the mixed-context reflection law: mixed nonunit witnesses (one identity-oriented nonunit and one reciprocal-oriented nonunit) must reflect down to an identity-oriented prime-axis witness.
proof idea
Assume a mixed pair of nonunit witnesses and, for contradiction, that no prime is identity-oriented. Prime-local orientation then forces every prime axis to be reciprocal under $\chi$.
From that global prime-reciprocal hypothesis, product-display compatibility and the character axioms yield that every nonunit orbit direction is reciprocal (via the upstream lemma that all-prime-reciprocal implies all-nonunit-reciprocal). Apply this to the mixed identity nonunit witness to obtain a reciprocal value on the same direction.
Cross-equivalence is symmetric and transitive, so the identity and reciprocal values glue to a self-reciprocal nonunit direction. That contradicts the elementary fact that a nonunit orbit direction is never cross-equivalent to its own reciprocal. Hence some prime must have been identity-oriented.
why it matters
This lemma closes the identity half of mixed-witness reflection under the native prime-local hypothesis. Downstream, PRCPrimeCalibrationForcesMixedNonunitIdentityWitnessReflectsPrimeWitnessTarget_proved applies it after prime calibration has already forced product-display compatibility, so calibration alone yields the reflection law.
That target feeds the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization results used to pin the PRC cost to the unique $J$-shape. In the broader forcing chain this sits under T5 $J$-uniqueness: characters that could flip prime axes independently would spoil the d'Alembert factorization that forces $J(x)=\cosh(\log x)-1$. Ruling out mixed nonunit identity without a prime identity witness is one algebraic gate on that uniqueness path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.