PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_no_mixed_prime_orientation
plain-language theorem explainer
Prime calibration forces identity-branch uniformity on native prime axes if and only if it forbids mixed identity/reciprocal orientations across those axes. Anyone tracking native-cost uniqueness or the PRC universal-foundation certificate will cite this equivalence. The proof is a two-line term that packages the already-proved one-way implications.
Claim. The following are equivalent: (i) every ratio character that is prime-direction calibrated is identity-branch uniform on native prime axes; (ii) every such character has no mixed prime orientation (no independent identity vs reciprocal choices on distinct prime axes).
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative structure is read. Prime-direction calibration means $\chi$ is already fixed on the native prime axes in the cost-compatible way. Two residual freedom targets remain: branch uniformity (if any identity-oriented native prime axis is present, every native prime axis sits on the identity branch) and no-mixed orientation (one cannot assign identity to some primes and reciprocal to others independently).
The module develops native-cost uniqueness by reducing cost characters to doubled-trace and d'Alembert structure, then closing orientation and factorization blockers. The two targets above are pure Prop interfaces: universal statements over calibrated characters concluding either PRCCharacterPrimeIdentityBranchUniform or PRCCharacterNoMixedPrimeOrientation.
Upstream, each direction is already a short theorem: uniformity implies no-mixing via the local branch-uniform lemma, and no-mixing implies uniformity once local prime-orientation control is available from the proved local target.
proof idea
Term-mode Iff.intro (angle-bracket constructor). Left-to-right applies PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_of_branch_uniformity, which introduces a calibrated character and hands the uniformity hypothesis to PRCCharacterNoMixedPrimeOrientation_of_branch_uniform. Right-to-left applies PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_no_mixed_prime_orientation, which uses the proved local prime-orientation target and then PRCCharacterPrimeIdentityBranchUniform_of_local_no_mixed_prime_orientation. No new arithmetic; pure packaging of the two implications.
why it matters
Native-cost uniqueness needs a single clean orientation story: either mixed prime orientations are impossible under calibration, or identity-branch uniformity is forced. This iff lets downstream certificates quote either formulation. It is consumed by prc_native_cost_uniqueness_blocker_certificate (the blocker package that records zero-calibrated factorization and signed-admissible refutation) and by prc_universal_foundation_conditional_certificate in UniversalFoundation (kernel, real complete ordered field, and trace-logic bundle).
In the broader Recognition chain this sits under cost uniqueness for the J-cost side of the forcing story (T5 J-uniqueness and the Recognition Composition Law), before mass-ladder and constant extraction. It does not itself force $\phi$ or $D=3$; it only collapses two orientation targets so the uniqueness certificate can treat them as one gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.