PRCPrimeCalibrationForcesNoMixedNonunitOrbitOrientationTarget
plain-language theorem explainer
Packages the branch-coupling claim that every prime-calibrated ratio character has no mixed nonunit orbit orientation: an identity-oriented nonunit direction cannot coexist with a reciprocal-oriented one. Native-cost uniqueness work cites it as a named Lean target Prop. Pure definitional packaging of a universal quantification; no proof content.
Claim. For every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is prime-direction calibrated (its generated cost agrees with canonical $J$-cost on every prime orbit), then $\chi$ has no mixed nonunit orbit orientation: identity orientation at one nonunit direction cannot coexist with reciprocal orientation at another.
background
In the Primitive Recognition Calculus, costs factor through ratio characters on RatioOrbit (signed numerator over nonzero distinction denominator). A ratio character $\chi$ is unit at the identity orbit and multiplicative up to cross-equivalence, remaining quotient-native rather than definitionally equal.
Prime-direction calibration means the cost generated from $\chi$ matches the canonical $J$-cost on every native prime orbit. The no-mixed property is the branch-coupling half of global nonunit orientation coherence: identity orientation at one nonunit direction forbids reciprocal orientation at any other. Local orientation existence is separated out.
The module isolates exact Lean targets for what still blocks native cost uniqueness. The identity event sits at the $J$-cost minimum $x=1$.
proof idea
Definitional abbreviation only. The body is the universal quantification over maps $\chi$: assume ratio-character axioms and prime-direction calibration, conclude the no-mixed nonunit orientation predicate. No tactics, no lemmas applied at this site.
why it matters
Named target in the Pass-25 native cost uniqueness blocker certificate, which records that uniqueness is not closed but splits the gap into exact Lean Props. Downstream lemmas show equivalent routes into the target (from full nonunit coherence, from identity-witness exclusion of reciprocals, from product no-mixed) and an iff with the identity-witness exclusion target.
The target has been refuted: prime calibration alone does not force branch-coupling. That refutation feeds the blocker certificate and tightens which extra hypotheses (beyond T5 $J$-uniqueness style calibration on primes) are still required for d'Alembert factorization uniqueness of the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.