PRCCharacterPrimeIdentityTraceCoherent_of_branch_uniform
plain-language theorem explainer
Branch uniformity of prime-identity orientation for a ratio-orbit character implies prime-identity trace coherence. Anyone closing the native-cost uniqueness blocker or the prime-calibration transport target cites this. The proof is a one-line term reuse: the two Props are definitionally the same quantifier stack, so the hypothesis applies verbatim.
Claim. Let $\chi$ be a map on rational orbits. If identity orientation of any native prime axis under $\chi$ forces identity orientation of every native prime axis (branch uniformity), then $\chi$ is prime-identity trace-coherent: whenever $\chi$ fixes one calibrated prime direction up to cross-equality, it fixes every calibrated prime direction up to cross-equality.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters act on these orbits. Prime axes are the directions associated to prime distinction-nats; identity orientation means the character fixes that prime direction up to the orbit cross-equality relation.
Prime-identity trace coherence says that identity orientation at one calibrated prime forces the same at every calibrated prime. The local ratio-character laws (multiplication and reciprocal) do not connect orientation choices across distinct primes, so this cross-prime relation is a separate obstruction.
Branch uniformity is the same quantifier stack under a different name. Its doc-comment records that the remaining obstruction is branch uniformity of orientation, not construction of the trace itself. Both Props quantify over pairs of prime orbits and transport identity orientation from one prime direction to the other.
proof idea
One-line term proof. Introduce the five binders of the target Prop (two primes, their prime-orbit witnesses, and the identity-orientation hypothesis at the first prime). Discharge by applying the branch-uniformity hypothesis to exactly those binders. No rewriting or lemmas are needed: the two definitions are definitionally identical.
why it matters
This is one direction of the in-module equivalence between branch uniformity and trace coherence, which packages the two names as interchangeable. Downstream, prime-calibration forcing of branch uniformity is rewritten as forcing of trace coherence by applying this implication to the calibrated character. It also appears in the native-cost uniqueness blocker certificate assembly, where the prime-identity transport obstruction is tracked under both namings.
In the Recognition forcing chain the native cost is the unique J-cost fixed by T5 and the Recognition Composition Law. Closing uniqueness of that cost on the PRC side requires that identity orientation cannot split across prime axes; this lemma is the definitional bridge that lets the blocker be stated either as a uniformity gap or as a missing trace link.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.