PRCCharacterPrimeIdentityRespectsCommonTraceExtension_iff_trace_coherence
plain-language theorem explainer
For a ratio-orbit map χ, the explicit common-trace transport rule for prime identity orientation is equivalent to bare cross-prime identity coherence. Anyone tracking the native-cost uniqueness blockers cites this to collapse the two formulations. The proof is a two-constructor Iff packing of the already-proved directions.
Claim. Let $\chi$ be a map on rational orbits. Then the following are equivalent: (i) whenever two prime-axis position traces sit inside a common finite trace extension $T$, identity orientation of $\chi$ on one prime axis forces identity orientation on the other; (ii) identity orientation of $\chi$ at any single 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 is recovered from such a character once orientation and d'Alembert-type laws are fixed.
Prime axes carry a distinguished identity orientation (cross-equality of $\chi$ on the prime direction with the prime direction itself). The ratio-character laws are local to multiplication and reciprocal, so they do not by themselves link orientation choices across distinct primes. Trace coherence supplies that missing cross-prime relation: identity at one calibrated prime forces identity at every calibrated prime.
The common-trace-extension form is a more explicit transport rule: if two prime-axis position traces are witnessed inside one finite $\delta$-trace extension, identity orientation transports between them. Both formulations live in the native-cost uniqueness development that isolates blockers for uniqueness of the PRC native cost.
proof idea
Term-mode Iff introduction. The forward direction applies PRCCharacterPrimeIdentityTraceCoherent_of_common_trace_extension, which instantiates the common-extension hypothesis at the sum orbit-position trace of the two primes. The reverse applies PRCCharacterPrimeIdentityRespectsCommonTraceExtension_of_trace_coherence, which routes through the comparable-trace intermediate and then specializes. No new arithmetic is done here.
why it matters
This equivalence lets the uniqueness pipeline treat the explicit common-extension transport rule and the bare cross-prime coherence statement as interchangeable. Downstream it feeds prc_native_cost_uniqueness_blocker_certificate, which packages the zero-calibrated factorization target and the refutation of the signed-admissible factorization target.
In the broader Recognition Science stack, native-cost uniqueness is the PRC-side counterpart of J-uniqueness (forcing-chain T5): the cost that satisfies the Recognition Composition Law must be the unique J-cost $J(x)=(x+x^{-1})/2-1$. Closing orientation-transport blockers is a necessary step before that uniqueness can be stated without residual character freedom across prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.