PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_iff_nonunit_coherent
plain-language theorem explainer
Prime calibration forcing no mixed identity/reciprocal orientations in orbit products is equivalent to forcing a single coherent orientation on all nonunit orbit directions. Native-cost uniqueness and universal-foundation certificates cite this bridge. The proof is the Iff pair of the two already-proved one-way implications.
Claim. The following are equivalent: (i) every ratio-orbit character that is prime-direction calibrated has no mixed identity/reciprocal factor orientations under native orbit multiplication; (ii) every such character has a single coherent orientation across all nonunit orbit directions.
background
In the primitive recognition calculus, a ratio-orbit character is a map on ratio orbits compatible with the multiplicative structure used to build the native cost. Prime-direction calibration fixes how the character treats prime generators, pinning identity versus reciprocal orientation on those directions.
Two Prop-valued targets package what calibration should force. The product no-mixing target asks that native multiplication never pairs an identity-oriented factor with a reciprocal-oriented factor. The nonunit orientation-coherence target is stronger on its face: every nonunit orbit direction shares one global orientation. The module notes that once coherence holds, mixed products are impossible by nonunit non-self-reciprocity.
Both directions of the comparison are already theorems in this file: coherence from no-mixing (via local orientation propagation), and no-mixing from coherence (by specializing the coherent character).
proof idea
Term-mode Iff introduction. The forward arrow is PRCPrimeCalibrationForcesNonunitOrbitOrientationCoherentTarget_of_product_no_mixed; the reverse is PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget_of_nonunit_coherent. No new algebra: the declaration only packages the two implications as a single equivalence.
why it matters
Native cost uniqueness in Recognition Science needs calibration to kill mixed-orientation factorizations that would spawn non-unique cost characters. Equating the product no-mixing target with global nonunit coherence lets later certificates treat either formulation as the same obligation.
Downstream, prc_native_cost_uniqueness_blocker_certificate and prc_universal_foundation_conditional_certificate sit on this layer of the PRC foundation stack. The equivalence is bookkeeping for the forcing path toward J-uniqueness (T5) and the Recognition Composition Law, not a new physical law: it collapses two blocker statements so the uniqueness certificate can close without double-counting hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.