PRCCharacterPrimeIdentityRespectsTraceConnected_of_trace_coherence
plain-language theorem explainer
Trace-coherence of prime-identity orientation on a ratio character implies that identity orientation transports along any finite δ-trace link between prime axes. Native-cost uniqueness arguments cite this one-way reduction when closing the prime-axis transport blocker. The proof ignores the connectivity hypothesis and applies coherence directly.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever $\chi$ is identity-oriented on one calibrated prime axis, it is identity-oriented on every calibrated prime axis. Then, for any two prime axes that are $\delta$-trace connected, 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 / nonzero-denominator display of a rational scale factor. Characters $\chi$ act on these orbits; the native cost is recovered from a character once orientation and calibration are fixed.
Prime-identity trace-coherence says identity orientation at one calibrated prime forces identity orientation at every calibrated prime. The doc-comment calls this "the missing cross-prime relation": local multiplicative and reciprocal laws do not by themselves link orientation choices on distinct prime axes.
Respecting prime-axis trace connection is the weaker, path-local form: identity orientation transports only when a finite $\delta$-trace component already joins the two axes. This module packages both propositions as blockers on the way to uniqueness of the native cost (the RS $J$-cost).
proof idea
Term-style tactic proof in two steps. Introduce the two primes, their primality witnesses, the unused connectivity hypothesis, and the identity-orientation hypothesis on the first axis. Discharge by applying the coherence hypothesis to those same data, dropping connectivity. No auxiliary lemmas are needed; coherence is strictly stronger than path-local transport.
why it matters
This is one half of the equivalence between path-local prime-identity transport and global trace-coherence. The converse direction and the packed iff sit immediately downstream. Calibration-to-transport targets also route through it: once prime calibration forces coherence, this lemma upgrades that to the transport target used by uniqueness arguments.
It feeds the native-cost uniqueness blocker certificate, which records which factorization and orientation targets are proved or refuted. In the broader RS forcing picture this is bookkeeping on the way to $J$-uniqueness (T5) and the Recognition Composition Law: without a controlled cross-prime orientation rule, the native cost character is not forced.
No open scaffold remains on this arrow; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.