PRCCharacterPrimeIdentityBranchUniform
plain-language theorem explainer
If a ratio-orbit character fixes any native prime axis under cross-equivalence, it fixes every native prime axis. Native-cost uniqueness proofs cite this as the branch-uniformity half of prime-identity transport. The body is a pure Prop packaging that universal quantification; no proof work lives here.
Claim. For a map $\chi$ sending ratio orbits to ratio orbits: if any native prime axis $p$ satisfies $\chi(p)\sim p$ under cross-multiplication equivalence of ratio orbits, then every native prime axis $r$ likewise satisfies $\chi(r)\sim r$.
background
In the Primitive Recognition Calculus, ratio orbits are signed-numerator / nonzero-denominator displays of rational data built from finite distinction orbits (DistinctionNat). Two ratio orbits are related by cross-equivalence when the scaled numerators balance as signed orbits; that is the internal PRC stand-in for rational equality.
A native prime orbit is a nonzero, non-unit distinction position with no nontrivial factorization. Each such prime has a preferred axis (prime direction) as a ratio orbit. A character $\chi$ is a self-map of ratio orbits; identity orientation of an axis means $\chi$ fixes that axis up to cross-equivalence (the axis sits at the identity event of observer forcing, the J-cost minimum at state $1$).
This module isolates uniqueness of the native cost functional. The present definition strips the transport statement down to pure branch uniformity: identity orientation cannot hold on one prime axis and fail on another.
proof idea
Definitional packaging only. The body is the quantified implication over pairs of prime orbits: cross-equivalence of $\chi$ on the first prime direction forces the same on the second. No tactics, no lemmas applied; downstream theorems treat the name as the branch-uniformity interface.
why it matters
This is the named obstruction remaining after trace construction is set aside. Downstream, it is equivalent to prime-identity trace coherence, to identity-iff-two on primes, and (under local orientation) to absence of distinct mixed prime-pair witnesses. It also matches respect for canonical additive trace on prime identity.
Parent results use it directly: mixed-pair witnesses become absurd under branch uniformity; no-mixed-prime-orientation follows by applying the universal quantifier; several iff bridges convert between this Prop and the trace-coherence / canonical-add-trace formulations used in native-cost uniqueness.
In the broader RS forcing picture this sits under cost uniqueness for the J-functional (T5 landmark: $J(x)=(x+x^{-1})/2-1$), ensuring characters cannot split prime axes between identity and reciprocal orientations when building the native cost from doubled trace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.