PRCCharacterPrimeOrientationCoherent
plain-language theorem explainer
A ratio character is prime-orientation coherent when it picks one global branch on every native prime axis: either the identity direction on all primes, or the reciprocal on all primes. Downstream uniqueness and admissibility arguments cite this Prop to rule out mixed prime witnesses. The body is a pure disjunction of two universal cross-equality statements; no proof work lives here.
Claim. A map $\chi$ on ratio orbits is prime-orientation coherent if either (i) for every native prime orbit $p$, $\chi$ sends the prime direction of $p$ to a ratio orbit cross-equivalent to that same prime direction, or (ii) for every such $p$, $\chi$ sends the prime direction to a ratio orbit cross-equivalent to its reciprocal.
background
In the Primitive Recognition Calculus, ratio orbits are the internal rational displays: a signed-orbit numerator over a nonzero distinction-orbit denominator. Cross-equivalence (crossEq) is the PRC stand-in for rational equality, defined by balanced scaled numerators under cross-multiplication on $\delta$-orbit positions.
Native primes are distinction-orbit positions that are nonzero, non-unit, and free of nontrivial factorization. Each such prime $p$ determines a prime direction: the ratio orbit pointing along that prime axis. The total reciprocal on ratio orbits mirrors $q \mapsto 1/q$ on $\mathbb{Q}$, sending zero to zero.
A ratio character is a self-map of ratio orbits used to generate a native cost. Orientation on a prime axis means whether the character keeps the prime direction or flips it to its reciprocal. Coherence demands that this choice be uniform across all primes.
proof idea
Definitional Prop, not a proved theorem. The body is the disjunction of two universal quantifications over native primes $p$: either $\chi(\mathrm{primeDir}(p))$ is cross-equivalent to $\mathrm{primeDir}(p)$ for every $p$, or it is cross-equivalent to $\mathrm{recip}(\mathrm{primeDir}(p))$ for every $p$. No tactics or lemmas are applied at the definition site; later theorems discharge one disjunct or the other.
why it matters
This Prop is the coherence gate in the native-cost uniqueness pipeline. It feeds the no-mixed-prime-witnesses theorem (coherent orientation implies no simultaneous identity and reciprocal prime witnesses), the admissibility target that every admissible character is prime-orientation coherent, and the bridge from local two-prime branch controls to global coherence.
Concrete characters already inhabit it: the absolute-value character and the identity character are proved coherent via the identity branch. The zero-character consequence and the two-prime branch-control converses also route through this definition. In the broader forcing story it keeps prime-axis data from mixing orientations before J-cost uniqueness and the RCL-driven cost reconstruction are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.