PRCCharacterPrimeIdentityTraceCoherent_of_comparable_trace
plain-language theorem explainer
If a ratio character transports prime identity orientation along any pair of comparable orbit traces, then it is fully trace-coherent: identity at one calibrated prime forces identity at every calibrated prime. Cited when collapsing the comparable-trace blocker to plain cross-prime coherence. The proof is a one-line application of universal orbit-trace comparability.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever two prime axes have $\delta$-orbit traces comparable by extension, identity orientation of $\chi$ on the first axis forces identity orientation on the second. Then identity orientation of $\chi$ at any calibrated prime forces identity orientation at every calibrated prime.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays (signed numerator over a nonzero distinction-nat denominator). Calibrated primes supply native axes primeDirection p hp. A character $\chi$ is identity-oriented on such an axis when RatioOrbit.crossEq holds between $\chi$ of that direction and the direction itself.
Prime identity trace coherence asks for a global cross-prime law: identity at one calibrated prime forces identity at every other. The local ratio-character laws (multiplication, reciprocal) do not supply this. The intermediate notion is respect for comparable traces: the same transport, but only when the finite $\delta$-orbit position traces of the two primes are related by Trace.Extends in either order.
Upstream, orbitPositionTrace_comparable proves that any two such position traces are always comparable by extension (by comparing the underlying toNat ranks). That structural fact is what turns the comparable-trace hypothesis into full coherence.
proof idea
Term-mode, three lines. Introduce primes $p,r$ with their prime-orbit witnesses and the identity hypothesis at $p$. Discharge the comparable-trace premise of the hypothesis by orbitPositionTrace_comparable p r, which yields the required Trace.Extends disjunction. Apply the comparable-trace respect hypothesis to conclude identity at $r$.
why it matters
This is one direction of the equivalence PRCCharacterPrimeIdentityRespectsComparableTrace_iff_trace_coherence, which identifies the comparable-trace blocker with plain prime-identity trace coherence. Downstream, PRCPrimeCalibrationForcesPrimeIdentityTraceCoherenceTarget_of_comparable_trace lifts the same reduction to the calibration-target layer, and the native-cost uniqueness blocker certificate records the surrounding factorization status.
In the Recognition framework this sits inside native-cost uniqueness for the PRC character: the missing cross-prime orientation law is exactly what would force a unique native cost compatible with the J-cost and the Recognition Composition Law. Closing or certifying this blocker is a step toward uniqueness of the cost that underwrites the forcing chain (T5 J-uniqueness onward).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.