PRCCharacterPrimeIdentityBranchUniform_of_trace_coherence
plain-language theorem explainer
Prime-identity trace coherence for a ratio-orbit character implies prime-identity branch uniformity: identity orientation on any calibrated prime axis forces it on every calibrated prime axis. Cited when discharging the native-cost uniqueness blocker and when packaging the two names as equivalent. The proof is a direct intro/exact transfer; the two propositions have identical bodies.
Claim. Let $\chi$ be a map on rational orbits. If $\chi$ is prime-identity trace-coherent (identity orientation at one calibrated prime forces identity orientation at every calibrated prime), then $\chi$ is prime-identity branch-uniform (the same cross-prime forcing, recorded under the branch-uniformity name).
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. Each prime of the distinction naturals determines a native prime axis (prime direction); identity orientation means the character fixes that axis up to the orbit cross-equality relation.
Local ratio-character laws only constrain multiplication and reciprocal. They do not by themselves link orientation choices on distinct prime axes. Trace coherence is exactly that missing cross-prime relation: identity orientation at one calibrated prime forces it at every calibrated prime.
Branch uniformity is definitionally the same proposition. The second name records that the remaining obstruction is uniformity of the identity branch across primes, not construction of a trace.
proof idea
Term-mode, essentially definitional. Introduce the two primes, their primality witnesses, and the identity-orientation hypothesis on the first axis; apply the trace-coherence hypothesis at those same data. No auxiliary lemmas: the two named Props share the same quantifier and implication body.
why it matters
Closes one direction of the equivalence between branch uniformity and trace coherence, so either name can be used in uniqueness arguments. Downstream, the calibration-forces-branch-uniformity target is obtained by feeding a calibration-forces-trace-coherence hypothesis through this implication. It also appears in the native-cost uniqueness blocker certificate chain, which packages factorization and signed-admissible targets for the uniqueness program.
In the Recognition forcing picture this sits under native J-cost uniqueness (T5-adjacent): characters must not freeload independent identity branches on different prime axes. The lemma does not invent new physics; it makes the naming split harmless so the blocker can be stated in either language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.