PRCCharacterPrimeIdentityRespectsCanonicalAddTrace_of_branch_uniform
plain-language theorem explainer
Branch-uniform prime-identity orientation for a ratio-orbit character immediately yields the canonical-add-trace transport law: if one native prime axis is identity-oriented, every other is, without needing finite δ-trace extension witnesses. Anyone closing the native-cost uniqueness blocker or the prime-calibration forcing chain cites this. The proof is a one-line term that discards the unused Trace.Extends hypotheses and applies the branch-uniformity assumption.
Claim. Let $\chi$ be a map on rational orbits. If $\chi$ is branch-uniform for prime identity (whenever any native prime axis is identity-oriented under $\chi$, every native prime axis is), then $\chi$ respects canonical add-trace transport: for native primes $p,r$, whenever the position traces of $p$ and of $r$ both extend to the position trace of $p+r$, identity orientation of the $p$-axis under $\chi$ forces identity orientation of the $r$-axis.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters $\chi$ act on these orbits. Native prime axes are the prime directions primeDirection p hp; identity orientation means $\chi$ fixes that axis up to RatioOrbit.crossEq.
PRCCharacterPrimeIdentityBranchUniform is the trace-free content of the prime-identity transport blocker: identity orientation on any one native prime axis forces it on every native prime axis. The doc records that the remaining obstruction is branch uniformity, not trace construction.
PRCCharacterPrimeIdentityRespectsCanonicalAddTrace strengthens the packaging: identity orientation must transport through the specific finite common extension orbitPositionTrace (p + r), removing arbitrary common-trace witnesses. The only remaining content is that the character respects the canonical finite $\delta$-trace merger of two prime axes. This module sits in the native-cost uniqueness development that isolates what still blocks uniqueness of the PRC cost character.
proof idea
One-line term proof. Introduce primes $p,r$, their primality witnesses, the two Trace.Extends hypotheses for the canonical merger $p+r$, and the identity-orientation hypothesis on the $p$-axis. Discard the two extension hypotheses (they are unused), and apply the branch-uniformity assumption directly to the remaining data. Branch uniformity already quantifies over all prime pairs with no trace side-conditions, so it is strictly stronger than the canonical-add-trace form and implies it immediately.
why it matters
This is one half of the equivalence PRCCharacterPrimeIdentityBranchUniform_iff_canonical_add_trace, which identifies the trace-free branch-uniformity blocker with its canonical-add-trace packaging. Downstream, PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget_of_branch_uniformity lifts a calibration-level branch-uniformity target to the canonical-add-trace target by applying exactly this theorem. The same direction feeds the native-cost uniqueness blocker certificate machinery that records what remains open in forcing the unique native cost character. In the broader Recognition forcing chain this sits under cost uniqueness (J-uniqueness / T5 territory): isolating that the last obstruction is pure branch uniformity, not an artifact of how finite $\delta$-traces are assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.