PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_successor_step_pair
plain-language theorem explainer
Prime calibration of ratio characters, once it forces the split one-step prime-floor successor identities (extend and contract), already forces a single coherent orientation on every nonunit orbit direction. Native-cost uniqueness and the universal-foundation certificate cite this implication. The proof is a pure two-step term composition through the product no-mixing intermediate.
Claim. Assume the prime-floor identity successor-step pair: both the one-step extend target and the one-step contract target hold. Then every ratio character $\chi$ that is prime-direction calibrated is nonunit-orbit orientation coherent, i.e. a single orientation is forced on all nonunit orbit directions.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ assign orbit data to ratio orbits and are constrained by native cost structure. Prime-direction calibration means $\chi$ is fixed on prime axes in the calibrated way. Nonunit-orbit orientation coherence is the global demand that every nonunit direction receives one and the same orientation (identity versus reciprocal), not a patchwork.
The hypothesis is the split one-step form of the corrected prime-floor successor target: the conjunction of the extend-successor and contract-successor one-step identities. The conclusion is the stronger coherence target that replaces mere product no-mixing: once a single orientation is forced on all nonunit directions, mixed product factors are ruled out by nonunit non-self-reciprocity.
Upstream, the product no-mixing target is already known to imply coherence, and the successor-step pair is known to imply product no-mixing (via an identity-comparable-trace bridge). This declaration only packages that chain.
proof idea
Pure term-mode composition, no tactics. First apply the upstream lemma that turns the successor-step pair hypothesis into the orbit-product no-mixed-orientation target. Feed that result into the upstream lemma that turns product no-mixing into nonunit-orbit orientation coherence. The whole proof is those two applications nested.
why it matters
Closes one direction of the local equivalence between nonunit-orbit orientation coherence and the prime-floor successor-step pair, so the two blocker faces can be swapped freely. That equivalence is consumed by the native-cost uniqueness blocker certificate, which packages zero-calibrated factorization and related refutations for the uniqueness program. The same target also appears in the universal-foundation conditional certificate, tying prime-calibration orientation control into the broader PRC foundation stack. In framework terms this is foundation plumbing under native cost uniqueness (the J-cost / RCL layer), not yet a T5–T8 forcing step, but it removes a branch-coupling obstruction that would otherwise block uniqueness of the native cost character.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.