PRCCharacterPrimeIdentityBranchUniform_iff_trace_coherence
plain-language theorem explainer
For a ratio-orbit character χ, branch uniformity of prime-identity orientation is equivalent to prime-identity trace coherence. Both assert that identity orientation on any native prime axis forces the same on every native prime axis. Anyone auditing the native-cost uniqueness blocker or the universal-foundation certificate cites this bridge. The proof is the pair of one-line direction wrappers.
Claim. For any map $\chi$ from ratio orbits to ratio orbits, the following are equivalent: (i) if $\chi$ is identity-oriented on any native prime axis, then it is identity-oriented on every native prime axis (branch uniformity); (ii) identity orientation at one calibrated prime forces identity orientation at every calibrated prime (trace coherence).
background
A ratio orbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters act as maps $\chi$ on ratio orbits. Native prime axes are the prime directions in this display; identity orientation means $\chi$ fixes that axis up to the cross-equality relation on ratio orbits.
Prime-identity trace coherence says identity orientation at one calibrated prime forces it at every calibrated prime. It is the missing cross-prime relation: the local ratio-character laws (multiplication and reciprocal) do not by themselves connect orientation choices on distinct prime axes.
Branch uniformity is definitionally the same proposition, renamed to record that the remaining obstruction is uniformity of orientation branches across primes, not construction of the trace itself. The module develops native-cost uniqueness for the Primitive Recognition Calculus, isolating blockers that prevent a unique native cost character.
proof idea
Term-mode proof: the biconditional is the pair of already-proved one-direction lemmas. Left-to-right applies the wrapper that turns branch uniformity into trace coherence by feeding the same quantifiers and hypothesis. Right-to-left applies the dual wrapper that turns trace coherence into branch uniformity the same way. No new arithmetic is done; the two named Props have identical bodies.
why it matters
This equivalence lets downstream certificates treat the two blocker names interchangeably. It is consumed by the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization targets and signed-admissible refutations, and by the universal-foundation conditional certificate (kernel, real complete ordered field, trace logic).
In the Recognition forcing chain the native cost is the J-cost $J(x)=(x+x^{-1})/2-1$ forced at T5; uniqueness of that cost on the ratio-orbit character is a foundation step before phi, the eight-tick octave, and $D=3$. The cross-prime identity-transport gap is exactly the obstruction these named Props isolate. Closing or discharging that blocker is what the uniqueness certificate tracks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.