PRCCharacterPrimeIdentityTraceCoherent_of_trace_connected
plain-language theorem explainer
If a ratio-orbit character transports identity orientation along any prime-axis δ-trace connection, then identity at one calibrated prime forces identity at every calibrated prime. Native-cost uniqueness arguments cite this to collapse the weaker transport rule to full cross-prime coherence. The proof feeds the already-proved fact that every pair of prime axes is trace-connected into the transport hypothesis.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever two prime axes are related by a finite $\delta$-trace connection and $\chi$ fixes the first prime direction up to cross-equality, it also fixes the second. Then identity orientation of $\chi$ at any one calibrated prime forces identity orientation at every calibrated prime.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-nat denominator. Characters $\chi$ act on these orbits; the native cost uniqueness program needs control of how $\chi$ orients the prime axes (the directions associated to prime distinction-nats).
Prime identity orientation is local unless something glues distinct primes. Trace coherence is that glue: if $\chi$ is identity-oriented on one calibrated prime axis, it must be identity-oriented on every calibrated prime axis. The weaker transport rule only asks that identity orientation move along a witnessed finite $\delta$-trace component between two primes.
Upstream, every pair of prime axes is already known to be trace-connected: PRCPrimeAxisTraceConnected_proved supplies an explicit orbit-position trace witnessing the connection. That global connectivity is what upgrades transport to full coherence.
proof idea
Term-mode introduction of the four prime-axis data and the identity hypothesis at $p$. Apply the transport hypothesis at those data, inserting PRCPrimeAxisTraceConnected_proved p hp r hr as the missing connectivity witness, then discharge with the given identity orientation at $p$. One application, no further rewriting.
why it matters
This is one direction of the equivalence between respecting prime-axis trace connection and full prime-identity trace coherence. Downstream, that equivalence feeds prc_native_cost_uniqueness_blocker_certificate, which packages the zero-calibrated factorization targets that block non-unique native costs.
In the Recognition framework the missing cross-prime relation is exactly what local ratio-character laws (multiplication and reciprocal) do not supply. Closing it is a step toward uniqueness of the native cost built from the J-cost fixed by the Recognition Composition Law and the T5 uniqueness of $J(x)=(x+x^{-1})/2-1$. Without coherence, orientation choices on distinct prime axes could drift and spoil a unique native cost character.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.