PRCCharacterPrimeIdentityRespectsComparableTrace_iff_trace_coherence
plain-language theorem explainer
For any map χ on ratio orbits, the prime-identity transport law under comparable δ-traces is equivalent to full cross-prime identity coherence. Anyone tracking the native-cost uniqueness blockers or the universal-foundation certificate will cite this. The proof is a two-constructor iff packaging the two already-proved directions, using that every pair of prime orbit traces is comparable.
Claim. Let $\chi$ be a map on ratio orbits. Then the following are equivalent: (i) whenever two prime axes have $\delta$-orbit traces comparable by extension and $\chi$ fixes the first prime direction up to cross-equality, it fixes the second; (ii) if $\chi$ fixes any calibrated prime direction up to cross-equality, it fixes every calibrated prime direction.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Prime axes are the directions of prime distinction-nats; identity orientation means $\chi$ sends a prime direction to a cross-equal copy of itself.
Two propositions package how identity orientation moves across primes. Trace coherence says identity at one calibrated prime forces identity at every calibrated prime: the missing cross-prime relation, since ordinary ratio-character laws are local to multiplication and reciprocal. The comparable-trace law is the same transport but gated on finite $\delta$-orbit traces being comparable by extension.
Upstream, structural comparability of any two orbit-position traces is already available, and the two one-way implications between the gated and ungated forms are proved separately. This declaration closes the loop.
proof idea
Term-mode packaging of an iff. The forward arrow is the already-proved lemma that comparable-trace respect implies full trace coherence: introduce primes $p,r$, feed the identity hypothesis, and discharge the gate with the global fact that any two orbit-position traces are comparable. The reverse arrow is the already-proved lemma that coherence implies comparable-trace respect: introduce primes and the comparability hypothesis, ignore the gate, and apply coherence. No new algebra is done here.
why it matters
Native-cost uniqueness needs a clean statement of the cross-prime identity blocker: either the gated trace-order form or the ungated coherence form may appear in certificates, and this iff lets them be swapped freely. Downstream it is consumed by the native-cost uniqueness blocker certificate and by the universal-foundation conditional certificate (kernel, real complete ordered field, and trace-logic legs). In the Recognition forcing picture this sits under the foundation layer that eventually feeds J-uniqueness and the RCL, by locking how identity orientation on prime axes can or cannot vary. It does not itself force the cost functional; it only equates two formulations of the orientation-transport obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.