PRCPrimeCalibrationForcesNonunitOrbitOrientationLocalComparableTraceTarget
plain-language theorem explainer
Conjunction target packing two prime-calibration obligations on ratio characters: every nonunit orbit gets a local orientation branch, and identity orientation respects finite δ-trace comparability across nonunit directions. Cited by the native-cost uniqueness blocker certificate and by the iff/projection lemmas that equate this pack with its identity-trace half. Defined as a plain Prop conjunction of those two component targets.
Claim. The following two statements hold simultaneously: (i) every ratio character that is prime-direction calibrated admits a local orientation on every nonunit orbit direction; (ii) every such character has identity orientation that respects comparability of finite $\delta$-orbit traces on nonunit directions.
background
In the primitive recognition calculus, a ratio character $\chi$ is a map on ratio orbits encoding multiplicative cost structure. Prime-direction calibration means $\chi$ is already fixed on prime axes. The first conjunct asks that this calibration extend to a local orientation branch on every nonunit orbit, not only primes.
The second conjunct is the trace-layer sharpening of identity-branch transport: instead of raw identity transport, one requires that identity orientation respect comparability of finite $\delta$-orbit traces on nonunit directions. The module packages native-cost uniqueness blockers as exact Lean targets; this definition is the trace-layer version of the active local identity-transport pack.
Upstream, the two halves are named separately: nonunit orbit local orientation under prime calibration, and nonunit identity comparable-trace under prime calibration. Their conjunction is the sharpened source of global nonunit coherence.
proof idea
No proof: this is a definitional abbreviation. The body is the propositional conjunction of the local-orientation target and the identity comparable-trace target. Downstream lemmas project with .1 / .2, rebuild the pair from either half via the known implication local-orientation $\leftarrow$ identity-comparable-trace, and transport from the older identity-transport pack by replacing the second half with its finite $\delta$-trace equivalent.
why it matters
This pack is the trace-layer successor of the local identity-transport target inside the native-cost uniqueness program. It feeds PRCNativeCostUniquenessBlockerCertificate, which records that native cost uniqueness is not closed but is split into exact Lean targets. Projection and iff theorems identify the pack with its identity-comparable-trace half, so refuting that half refutes the whole conjunction (..._refuted).
In the Recognition forcing chain this sits under T5 J-uniqueness and the Recognition Composition Law: native cost is meant to be the unique J-shaped cost on ratio characters. The definition isolates the nonunit-orbit coherence gap that still blocks uniqueness. A later theorem already refutes the target, so the blocker certificate can mark this branch closed negatively rather than leave it open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.