PRCCharacterPrimeIdentityRespectsComparableTrace_of_trace_coherence
plain-language theorem explainer
Trace coherence of prime-identity orientation on a ratio character immediately yields the comparable-trace transport law: identity at one calibrated prime forces identity at every prime whose finite δ-orbit traces are comparable by extension. Native-cost uniqueness arguments cite this as one direction of the coherence/comparable-trace equivalence. The proof ignores the comparability hypothesis and applies coherence directly.
Claim. Let $\chi$ be a map on ratio orbits. If identity orientation of $\chi$ at any calibrated prime forces identity orientation at every calibrated prime (trace coherence), then whenever two prime axes have finite $\delta$-orbit traces comparable by extension, identity orientation of $\chi$ on the first axis forces identity orientation on the second.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator: the display type for rational directions built from signed orbits. Calibrated primes supply distinguished axes via prime directions; a ratio character $\chi$ may or may not fix those axes up to the cross-equality relation on orbits.
Trace coherence says identity orientation at one calibrated prime forces identity at every calibrated prime. That cross-prime link is not implied by the local multiplicative and reciprocal laws on characters alone. The comparable-trace law is the ordered variant: identity transports only between primes whose finite $\delta$-orbit position traces are related by the extends relation (either way).
The module develops native-cost uniqueness for characters. Structural comparability of any two orbit traces is already available upstream, so the remaining content is whether the character respects that order when carrying identity orientation.
proof idea
Term-style one-step reduction. Introduce the two primes, their primality witnesses, the unused comparability disjunction, and the identity hypothesis on the first prime. Discharge by applying the coherence hypothesis to those same data; coherence already concludes identity on the second prime with no appeal to trace extension. Comparability is discarded as _.
why it matters
Closes one arrow of the equivalence between trace coherence and the comparable-trace identity law, and is the bridge used to lift coherence to the common-trace-extension form. Downstream, prime-calibration targets that force coherence are rewritten as comparable-trace targets by applying this lemma. It also appears in the native-cost uniqueness blocker certificate chain, which packages the factorization and signed-admissible refutation obligations for the uniqueness program.
In framework terms this is foundation plumbing under the J-cost uniqueness story (T5): characters must not flip prime axes independently if the native cost is to be forced. The lemma itself is purely logical strength comparison, not a new physical constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.