PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_of_product_no_mixed
plain-language theorem explainer
Prime calibration that forbids mixed identity/reciprocal orientations under orbit products already forces the split one-step prime-floor successor pair (extends and contracts). Anyone closing the native-cost uniqueness blocker or the product-no-mix ↔ successor-step equivalence cites this. The proof is a two-step term composition through the nonunit identity-comparable-trace intermediate.
Claim. Assume prime calibration forces the product no-mixing property: every ratio character that is prime-direction calibrated has no mixed identity/reciprocal factor orientations under native orbit multiplication. Then prime calibration also forces the split prime-floor successor pair: the identity orientation both extends and contracts by one successor step on the prime floor.
background
In Primitive Recognition Calculus, ratio characters assign oriented orbits to ratio orbits. Prime-direction calibration fixes orientation on prime axes. The product no-mixing target asks that this calibration rule out mixed identity versus reciprocal factor orientations when orbits multiply natively: once every nonunit direction is coherently oriented, mixed product factors are impossible by nonunit non-self-reciprocity.
The prime-floor successor pair is the split one-step form of the corrected prime-floor successor target. It is the conjunction of an extends-step target and a contracts-step target: identity orientation should both push forward and pull back by one successor step on the prime floor, not merely on prime axes.
This module builds the native-cost uniqueness ladder toward J-uniqueness (T5). Upstream, product no-mixing already yields the nonunit identity-comparable-trace target (via branch transport), and that comparable-trace target yields the successor-step pair (via successor transport).
proof idea
Pure term composition, no tactics. First apply the upstream lemma that product no-mixing implies the nonunit identity-comparable-trace target. Feed that conclusion into the upstream lemma that identity-comparable trace implies the prime-floor identity successor-step pair (itself a wrapper through successor transport). The hypothesis is used once; the result is the desired conjunction of extends and contracts.
why it matters
This is one direction of the local equivalence between product no-mixing and the successor-step pair, used immediately by PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_successor_step_pair. That equivalence collapses two blocker faces into one, so either formulation can discharge the native-cost uniqueness blocker certificate.
Downstream it feeds prc_native_cost_uniqueness_blocker_certificate and, through the foundation stack, prc_universal_foundation_conditional_certificate. In the Recognition forcing chain this sits under T5 J-uniqueness: native cost must be the unique d'Alembert/RCL cost $J(x)=(x+x^{-1})/2-1$, and prime calibration must force coherent orientation so no rival cost character survives. Closing product-no-mix versus successor-step removes a fork in that uniqueness ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.