PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget
plain-language theorem explainer
Prime calibration of a ratio-orbit character is packaged as forcing global nonunit orientation coherence: every nonunit direction is identity-oriented, or every one is reciprocal-oriented. Native-cost-uniqueness work cites this as the stronger replacement for product no-mixing. Once available, mixed product factors are ruled out by nonunit non-self-reciprocity. The declaration is a pure Prop target with no proof body.
Claim. For every map $\chi$ from rational orbits to rational orbits, if $\chi$ is a ratio character and is prime-direction calibrated, then the nonunit orbit orientation of $\chi$ is coherent: either every nonunit direction is identity-oriented, or every nonunit direction is reciprocal-oriented.
background
In the Primitive Recognition Calculus, a rational orbit is an integer numerator over a nonzero orbit denominator. Characters on these orbits encode how recognition ratios transform under the ledger. Two canonical orientations appear: the identity event at the J-cost minimum $x=1$, and the reciprocal event that swaps source and target with inverted ratio.
Nonunit orbit orientation coherence means every nonunit orbit direction chooses the same branch, all identity or all reciprocal. Upstream documentation states this is exactly the coherence strong enough to rule out mixed product factors. Prime-direction calibration is the local constraint that primes pick a preferred orientation.
This module develops uniqueness of the native cost built from such characters. The present definition packages the claim that prime calibration alone upgrades local prime data to global nonunit orientation coherence, replacing weaker product no-mixing targets.
proof idea
Definitional packaging only. The body is the quantified proposition itself: for all maps $\chi$ on rational orbits, ratio-character plus prime-direction calibration implies nonunit orbit orientation coherence. No tactics, no lemmas, and no reduction steps are applied.
why it matters
This target is the stronger replacement for product no-mixing in the native cost uniqueness program. Downstream reductions take it as a hypothesis and discharge weaker targets: no mixed nonunit orientation, nonunit branch agreement, identity branch transport, identity-witness globalization, and local nonunit orientation. It also appears in the Pass-25 blocker certificate that splits unfinished uniqueness mathematics into exact Lean targets.
Once proved, mixed product factors become impossible by nonunit non-self-reciprocity, tightening the path to a unique native cost. That uniqueness sits under the broader forcing chain: J-uniqueness (T5) and the Recognition Composition Law constrain admissible costs, and coherent orientation is the discrete character-level step that keeps factorizations from mixing identity and reciprocal branches.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.