PRCCharacterNonunitIdentityRespectsComparableTrace_of_prime_comparable
plain-language theorem explainer
Under a ratio character with product-display compatibility and local prime orientation, the prime-axis identity transport law upgrades to the same law for every nonunit orbit direction. Anyone proving native-cost uniqueness via d'Alembert factorization of the PRC cost cites this step. The proof reduces a nonunit identity witness to a prime witness, spreads identity across all primes by trace comparability, then lifts back to the target nonunit.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence). Assume $\chi$ respects native orbit-product displays, sends each prime direction to itself or its reciprocal, and transports identity orientation between any two primes whose finite $\delta$-orbit traces are comparable by extension. Then identity orientation at one nonunit orbit direction transports to any other nonunit direction whenever their orbit traces are comparable.
background
Primitive Recognition Calculus works with finite distinction orbits DistinctionNat and rational displays RatioOrbit (signed numerator over nonzero orbit denominator). Equality of displays is the internal cross-multiplication relation crossEq, not definitional equality, so characters stay quotient-native.
A PRCRatioCharacter is a map $\chi$ on ratio orbits that fixes the unit, multiplies, and inverts, all up to crossEq. It is the candidate factor in a d'Alembert factorization of a PRC cost. Local prime orientation says each prime axis is sent to itself or its reciprocal: the algebraic content of equal $J$-costs on a single prime direction. Product-display compatibility is the extra quotient-respect step that makes $\chi$ agree on a product orbit and on the ratio product of its factors.
The conclusion is the trace-order form of nonunit identity transport: if one nonunit direction is on the identity branch, every nonunit with a comparable finite $\delta$-orbit trace is too. Orbit traces are always comparable (orbitPositionTrace_comparable), so this is equivalent to global nonunit identity-branch transport, packaged as a trace-order law.
proof idea
Tactic proof. Fix nonunits $p,r$ with comparable traces and identity at $p$. Apply PRCCharacterNonunitIdentityWitnessReflectsPrimeWitness_of_prime_local (using the character, product compatibility, and local prime orientation) to extract a prime $q$ that also sits on the identity branch.
From the prime identity-transport hypothesis and structural comparability of any two orbit traces, conclude that every prime direction is identity-oriented. Feed that global prime-identity fact into PRCCharacterNonunitOrbitAllIdentity_of_all_prime_identity to obtain identity at the target nonunit $r$.
why it matters
Native-cost uniqueness in PRC needs the character branch to be coherent: identity on one nonunit cannot flip on another. This theorem is the bridge from the prime-axis transport law to the full nonunit transport law under the standing character hypotheses.
It is consumed by PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_prime_identity_comparable_trace, which lifts a prime-calibration hypothesis to the nonunit comparable-trace target. That sits on the path toward uniqueness of the cost factor, aligning with the framework landmark T5 ($J$-uniqueness, $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law that forces the same functional form.
No scaffolding remains here: the claim is fully proved and only packages prior local and prime-level lemmas into the nonunit statement the calibration chain needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.