PRCCharacterMixedNonunitReciprocalWitnessReflectsPrimeWitness_of_prime_local
plain-language theorem explainer
Under prime-local orientation and product-display compatibility, a ratio character that mixes identity and reciprocal orientations on nonunit orbits must already invert some prime axis. Cost-uniqueness and prime-calibration arguments cite this reflection law. The proof forces all primes to the identity branch, lifts that to every nonunit, then contradicts a reciprocal nonunit witness via non-self-reciprocity of nonunit directions.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence). Assume $\chi$ respects native orbit-product displays, and that on every prime direction $\chi$ acts as the identity or the reciprocal. Then whenever $\chi$ is the identity on some nonunit orbit and the reciprocal on another, there exists a prime $p$ such that $\chi$ sends the prime direction of $p$ to its reciprocal (up to cross-equivalence).
background
Primitive Recognition Calculus works with distinction naturals and ratio orbits: a ratio orbit is a signed numerator over a nonzero distinction denominator. Equality is the internal cross-multiplication relation crossEq (balanced scaled numerators), not definitional equality, so characters stay quotient-native.
A ratio character $\chi$ is a map on ratio orbits that fixes the unit, multiplies, and intertwines reciprocal, all up to crossEq. Product-display compatibility is the extra quotient-respect step: $\chi$ on a composite orbit agrees with $\chi$ on the product of the factor directions. Prime-local orientation says each prime axis is sent either to itself or to its reciprocal; that is the algebraic content of matching $J$-costs on a single prime direction.
The target property is the reciprocal half of the mixed-context reflection law: if there is both an identity-oriented nonunit witness and a reciprocal-oriented nonunit witness, then some prime axis must already be reciprocal-oriented.
proof idea
Assume a mixed pair of nonunit witnesses and, for contradiction, that no prime is reciprocal-oriented. Prime-local orientation then collapses to identity on every prime direction.
Apply PRCCharacterNonunitOrbitAllIdentity_of_all_prime_identity (using the character axioms and product-display compatibility) to lift prime identity to identity on the reciprocal nonunit witness $r$. Transitivity and symmetry of crossEq then give that the native direction of $r$ is cross-equivalent to its own reciprocal.
Close with orbitDirection_nonunit_not_crossEq_recip: a nonunit orbit direction cannot be cross-equivalent to its reciprocal. That contradiction forces a reciprocal prime witness.
why it matters
This lemma is a local algebraic step in native cost uniqueness for PRC characters. Downstream, PRCPrimeCalibrationForcesMixedNonunitReciprocalWitnessReflectsPrimeWitnessTarget_proved packages it under prime calibration (supplying product-display compatibility from the calibration target), and the uniqueness blocker certificate records the corresponding factorization targets.
In the Recognition forcing chain, uniqueness of the cost functional is the T5 landmark: $J(x)=(x+x^{-1})/2-1$ is the unique admissible generator compatible with the Recognition Composition Law. Here the work is at the discrete orbit level: mixed reciprocal orientations cannot hide on composite nonunits; they must already appear on a prime axis. That blocks independent prime-axis inversions from spoiling a unique native factorization of the doubled-trace cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.