PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_successor_step_pair
plain-language theorem explainer
Equates two formulations of the prime-calibration forcing goal: ruling out mixed identity/reciprocal orientations under native orbit multiplication, versus the split one-step prime-floor successor pair (extends and contracts). Native-cost uniqueness and universal-foundation certificates cite this bridge. The proof is a pure Iff constructor from the two already-proved one-way implications.
Claim. The assertion that every prime-direction-calibrated ratio character has no mixed identity/reciprocal factor orientations under native orbit multiplication is equivalent to the assertion that prime calibration forces both the extending and the contracting one-step prime-floor identity successor conditions.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ assign to each ratio orbit another orbit, subject to multiplicative and reciprocity constraints. Prime-direction calibration orients $\chi$ on prime axes so that the native cost (the doubled-trace $J$-type functional) is coherent with the Recognition Composition Law.
Two blocker targets package what calibration is expected to force. The product no-mixing target asks that $\chi$ never multiplies an identity-oriented factor by a reciprocal-oriented factor on nonunit orbits. The successor-step pair is the conjunction of an extending one-step and a contracting one-step prime-floor identity condition: calibration should push every nonunit direction consistently forward and backward along the prime floor.
Both targets sit in the native-cost uniqueness module, whose aim is to pin the cost functional to the unique $J$ of the forcing chain (T5).
proof idea
Term-mode Iff introduction. The forward direction is the existing lemma that product no-mixing yields the successor-step pair (via the intermediate nonunit identity-comparable-trace target). The reverse direction is the existing lemma that the successor-step pair yields product no-mixing (again through that intermediate). No new algebra is done here; the declaration only packages the two arrows as $\leftrightarrow$.
why it matters
Native-cost uniqueness needs interchangeable formulations of the prime-calibration blocker so certificates can discharge whichever shape is convenient. Downstream, prc_native_cost_uniqueness_blocker_certificate and the conditional universal-foundation certificate consume this bridge when assembling the uniqueness package.
In the broader RS chain this is scaffolding around T5 $J$-uniqueness: once prime calibration forces a single coherent orientation, mixed product factors are impossible by nonunit non-self-reciprocity, and the doubled-trace cost collapses to $J(x)=\cosh(\log x)-1$. The equivalence keeps the successor-step and product-no-mixing routes interchangeable without duplicating proof burden.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.