PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget_of_identity_comparable_trace
plain-language theorem explainer
Under the hypothesis that prime calibration forces identity-branch orientation to respect comparable finite δ-orbit traces on nonunit directions, prime calibration also forces local orientation on every nonunit orbit direction. Native-cost uniqueness and the universal-foundation certificate cite this implication. The proof is a short term application: proved prime-axis orientation plus product-factor propagation (from the hypothesis) yield full nonunit local orientation.
Claim. Assume that every prime-direction-calibrated ratio character has identity-branch orientation that respects comparability of finite $\delta$-orbit traces on nonunit directions. Then every such character is locally oriented on every nonunit orbit direction, not only on prime axes.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how recognition cost orients multiplicative directions. Prime-direction calibration means $\chi$ is already fixed on prime axes. Local orientation on an orbit direction means the character chooses a coherent branch (identity vs reciprocal) at that direction.
The conclusion target asks that prime calibration force local orientation on all nonunit orbit directions, not merely primes. That is the first component of the prime-floor successor blocker for native-cost uniqueness.
The hypothesis is a trace-order sharpening: identity orientation on nonunit directions must respect comparability of finite $\delta$-orbit traces. An upstream lemma already shows that prime local orientation together with product-factor propagation of orientation through composite orbit positions implies full nonunit local orientation. Another upstream result derives that product-propagation target from the identity-comparable-trace hypothesis.
proof idea
Term-mode, three ingredients. Fix a ratio character $\chi$ that is prime-direction calibrated. Obtain prime-axis local orientation from the already-proved prime-orientation target. Obtain product-factor local-orientation propagation by applying the sibling implication that turns the identity-comparable-trace hypothesis into the product-propagation target, then specializing to $\chi$. Feed both into the combination lemma: prime local orientation plus product propagation yields nonunit orbit local orientation. Discharge the goal by that exact application.
why it matters
This closes the first half of the prime-floor successor blocker under a single named hypothesis (identity-comparable trace). Downstream, the paired target packages this implication with the hypothesis itself as a conjunction, and the native-cost uniqueness blocker certificate consumes the surrounding orientation stack. The universal-foundation conditional certificate also depends on this layer of the PRC uniqueness chain.
In the Recognition Science forcing picture, native cost uniqueness is the bridge from the Recognition Composition Law and J-uniqueness (T5) to a single admissible cost on ratio orbits. Orienting composite (nonunit) directions from prime calibration is the algebraic step that keeps the character from freeloading on composite axes. The remaining open piece is discharging the identity-comparable-trace hypothesis itself; this theorem only reduces the orientation target to that hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.