PRCCharacterPrimeIdentityBranchUniform_of_canonical_add_trace
plain-language theorem explainer
If a ratio-orbit character transports identity orientation through the canonical finite add-trace merger of two prime axes, then identity orientation is uniform across all native primes: one identity-oriented prime forces every prime to be identity-oriented. Cited by the iff linking branch uniformity to canonical add-trace and by the prime-calibration forcing target. Proof is a short term application of the two orbit-position add-extension lemmas.
Claim. Let $\chi$ be a map on rational orbits. Suppose that whenever $p$ and $r$ are prime distinction-naturals and identity orientation of $\chi$ on the $p$-axis is given, identity orientation transports to the $r$-axis through the canonical common extension $\mathrm{orbitPositionTrace}(p+r)$ (with the two $\mathrm{Trace.Extends}$ hypotheses). Then $\chi$ has prime identity branch uniformity: if any native prime axis is identity-oriented under $\chi$, every native prime axis is.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-natural denominator. Characters $\chi$ act on these orbits; identity orientation of a prime axis means $\chi$ fixes the prime direction up to the cross-equality relation on ratio orbits.
Prime identity branch uniformity is the trace-free transport law: identity orientation on one native prime forces it on every native prime. The canonical-add-trace variant strengthens the witness by requiring transport only through the specific finite $\delta$-trace merger $\mathrm{orbitPositionTrace}(p+r)$, rather than an arbitrary common extension. As the sibling doc states, this "removes the arbitrary witness from common-trace transport; the only remaining content is that the character respects the canonical finite $\delta$-trace merger of two prime axes."
Two elementary extension facts sit upstream: the position trace of $p$ always extends to that of $p+r$, and likewise for $r$ (via add-commutativity). Those facts discharge the two $\mathrm{Trace.Extends}$ premises of the canonical form automatically.
proof idea
Term-mode one-liner. Unfold branch uniformity and introduce primes $p,r$ with the identity-orientation hypothesis on $p$. Feed the canonical-add-trace hypothesis the two always-true extension lemmas $\mathrm{orbitPositionTrace_add_extends_left},p,r$ and $\mathrm{orbitPositionTrace_add_extends_right},p,r$, together with the given identity hypothesis. The conclusion is identity orientation on $r$. No further casework.
why it matters
This is one direction of the equivalence between branch uniformity and canonical add-trace respect, assembled immediately downstream as the iff theorem. That equivalence lets the uniqueness pipeline treat the two formulations interchangeably when discharging the prime-identity transport blocker.
It is also the bridge used by $\mathrm{PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_canonical_add_trace}$: once prime calibration is known to force the canonical-add-trace form, this lemma upgrades the conclusion to full branch uniformity. Both sit on the path into the native-cost uniqueness blocker certificate, which packages the zero-calibrated factorization targets that pin down the native $J$-cost character.
In the broader Recognition forcing chain this is foundation-level scaffolding for T5-style $J$-uniqueness: characters on ratio orbits must not flip identity orientation across prime axes if they are to match the unique cost functional $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.