PRCCharacterPrimeIdentityTraceCoherent
plain-language theorem explainer
Prime-identity orientation for a ratio character is trace-coherent when identity orientation on one calibrated prime axis forces the same on every calibrated prime. Ratio-character laws alone are local to multiplication and reciprocal, so this packages the missing cross-prime link. Downstream uniqueness and transport lemmas cite it as the common core of branch uniformity and several trace-respect conditions. The body is a pure Prop abbreviation, not a proved statement.
Claim. A map $\chi$ on ratio orbits is prime-identity trace-coherent when, for any two native primes $p$ and $r$, if $\chi$ sends the prime direction of $p$ to a ratio orbit cross-equivalent to that same direction, then $\chi$ likewise sends the prime direction of $r$ to a ratio orbit cross-equivalent to itself.
background
In the Primitive Recognition Calculus, rationals appear as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are related by cross-equivalence when the cross-multiplied signed orbits balance (the internal PRC stand-in for ordinary rational equality). Distinction nats carry a native primality predicate: nonzero, non-unit, and free of nontrivial factorization.
A ratio character $\chi$ acts on these displays. Along each calibrated prime one forms a prime direction; identity orientation at that axis means $\chi$ fixes the direction up to cross-equivalence. The module develops native cost uniqueness from character data, and the local character laws (multiplication, reciprocal) do not by themselves tie orientation choices on distinct prime axes.
The identity event in the broader forcing picture sits at the J-cost minimum $x=1$. Here the analogous notion is identity orientation of a prime axis under $\chi$, and the present definition isolates the global coherence of that choice across primes.
proof idea
No proof: this is a Prop-valued definition. The body is the universal quantification over pairs of native primes $p,r$ of the implication that identity orientation (cross-equivalence of $\chi$ on the prime direction with the direction itself) at $p$ yields the same at $r$. Downstream one-line wrappers simply apply this quantifier, or package it as an iff with branch uniformity and with several trace-respect predicates.
why it matters
This is the missing cross-prime relation in the native-cost uniqueness stack. Local ratio-character laws never connect orientation choices on different prime axes; packaging that link as a single Prop lets the module prove that branch uniformity, respect for comparable traces, common trace extensions, and trace-connectedness are all equivalent to this coherence condition.
Parent results include the iff and of-trace-coherence theorems for branch uniformity and for the various trace-respect predicates. Those feed the prime-identity transport story: once any native prime axis is identity-oriented, every native prime axis is, so the remaining obstruction is branch uniformity rather than trace construction. In the Recognition forcing chain this sits under the foundation layer that forces the unique J-cost and the self-similar structure used later for $\varphi$ and the octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.