PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_iff_successor_step_pair
plain-language theorem explainer
Equates two blocker formulations under prime calibration: global coherence of orientation on all nonunit ratio-orbit directions, versus the split one-step prime-floor identity successor pair (extends and contracts). Cited by anyone wiring the native-cost uniqueness blocker or the conditional universal-foundation certificate. Proof is a two-constructor packaging of the already-proved directions.
Claim. The following are equivalent: (i) every ratio-orbit character that is prime-direction calibrated is nonunit-orbit orientation coherent; (ii) prime calibration forces both the one-step extend and the one-step contract prime-floor identity successor targets.
background
In the Primitive Recognition Calculus, a ratio character is a map on ratio orbits compatible with the multiplicative structure used to build the native cost. Prime-direction calibration pins the character on prime axes. Nonunit-orbit orientation coherence is the stronger global demand that every nonunit orbit direction share one orientation (identity versus reciprocal), ruling out mixed product factors via nonunit non-self-reciprocity.
The successor-step pair target is the split one-step form of the corrected prime-floor successor: the conjunction of an extend step and a contract step for identity-oriented prime-floor transport. The module treats these as interchangeable blockers on the path to uniqueness of the native cost character.
Upstream, each direction of the equivalence is already available: coherence implies the successor pair via successor transport, and the successor pair implies coherence via product no-mixed orientation.
proof idea
Term-mode biconditional. The forward arrow applies the theorem that nonunit-orbit orientation coherence yields the prime-floor identity successor-step pair (via successor transport). The reverse arrow applies the theorem that the successor-step pair yields nonunit-orbit orientation coherence (via the product no-mixed intermediate). No new algebra is done here; the proof is pure packaging of those two lemmas into an Iff.
why it matters
Closes a local interface gap in the native-cost uniqueness blocker stack: either formulation of the prime-calibration orientation force may be used interchangeably. Downstream it is consumed by prc_native_cost_uniqueness_blocker_certificate, which assembles the zero-calibrated factorization and signed-admissible refutation pieces, and by the conditional universal-foundation certificate in UniversalFoundation.
In the broader Recognition chain this sits inside the foundation layer that forces the unique native cost (the J-cost side of T5 uniqueness and the RCL), before constants and the phi-ladder are specialized. It does not itself prove uniqueness; it only equates two remaining orientation blockers so later certificates can cite whichever form is convenient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.