PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_successor_step_pair
plain-language theorem explainer
Assuming the prime-floor identity successor-step pair (extension and contraction one-steps), prime calibration forces the product no-mixing target: no mixed identity/reciprocal factor orientations under native multiplication of ratio orbits. Native-cost uniqueness blockers and the orientation-coherence lift cite this implication. The proof is a two-step term composition through the identity-comparable-trace intermediate and its equivalence with product no-mixing.
Claim. If the prime-floor identity successor-step pair holds (both the one-step extension and one-step contraction targets for the corrected prime-floor identity), then every ratio-orbit character that is prime-direction calibrated has no mixed identity/reciprocal factor orientations under native multiplication.
background
In the Primitive Recognition Calculus, ratio orbits carry multiplicative structure, and a ratio character $\chi$ assigns an orbit image to each orbit. Prime-direction calibration constrains how $\chi$ acts on prime axes. The product no-mixing target asks that, once $\chi$ is a ratio character and prime-calibrated, native multiplication never mixes an identity-oriented factor with a reciprocal-oriented factor.
The hypothesis is the split one-step form of the corrected prime-floor successor target: the conjunction of the identity-extends and identity-contracts successor-step props. Upstream, that pair already yields the nonunit identity-comparable-trace target (via prime-floor successor transport). A sibling equivalence identifies product no-mixing with that identity-comparable-trace target, so the pair is enough to discharge no-mixing.
proof idea
Pure term proof, no tactics. Apply the upstream theorem that the successor-step pair implies the nonunit identity-comparable-trace target. Feed that conclusion into the reverse direction of the sibling equivalence between product no-mixing and identity-comparable-trace (.mpr). The composite is exactly the product no-mixing target.
why it matters
This is a link in the prime-calibration forcing chain inside PRC native-cost uniqueness. Downstream it feeds the orientation-coherence target (no-mixing plus nonunit non-self-reciprocity gives a single coherent orientation on nonunit orbits) and the iff that equates product no-mixing with the successor-step pair itself. Both the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate sit above this layer.
In the broader Recognition Science stack, native-cost uniqueness is the PRC-side route toward the unique $J$-cost of the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). Closing product orientation under prime calibration is a necessary algebraic step before the cost functional can be forced uniquely from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.