PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_iff_identity_forces_two
plain-language theorem explainer
The reciprocal-branch distinguished-axis forcing target is equivalent to the identity-branch one: under prime-direction calibration, forcing reciprocal orientation from any native prime axis onto orbit-2 is the same as forcing identity from any native prime axis onto orbit-2. Native-cost uniqueness and blocker-certificate arguments cite this bridge. Proof is a pure Iff constructor from the two already-proved one-way implications.
Claim. The following two propositions are equivalent. (A) For every ratio character $\chi$ that is prime-direction calibrated, if any native prime axis is reciprocal-oriented then the orbit-$2$ prime axis is reciprocal-oriented. (B) For every such $\chi$, if any native prime axis is identity-oriented then the orbit-$2$ prime axis is identity-oriented.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how a native cost functional orients each prime axis (identity branch versus reciprocal branch). Prime-direction calibration restricts $\chi$ so that distinguished prime axes sit in a fixed orientation class.
Two one-sided globalization targets appear. The reciprocal target asserts: once any calibrated native prime axis is reciprocal, the orbit-$2$ axis must also be reciprocal. The identity target asserts the dual: identity at any calibrated native prime forces identity at orbit-$2$. Both are universal statements over characters satisfying the ratio-character and prime-calibration hypotheses.
The surrounding module develops native-cost uniqueness via doubled-trace and d'Alembert structure on these characters. The two targets are the distinguished-axis halves of reciprocal versus identity globalization; this declaration equates them before either is discharged or refuted.
proof idea
Term-mode Iff introduction. The forward direction applies PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_of_prime_reciprocal_forces_two, which turns a proof of the reciprocal target into a proof of the identity target. The reverse applies PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_of_identity_forces_two. No new character-level reasoning occurs here; the declaration only packages the two one-way lemmas as an equivalence.
why it matters
This equivalence is the bridge used to refute the reciprocal target from the already-refuted identity target: PRCPrimeCalibrationForcesPrimeReciprocalForcesTwoPrimeReciprocalTarget_refuted applies .mp of this iff and hands the result to the identity-side refutation. That refutation feeds the native-cost uniqueness blocker certificate (prc_native_cost_uniqueness_blocker_certificate), which records which factorization and orientation targets survive.
Downstream, the universal-foundation conditional certificate also depends on this cluster. In the Recognition forcing chain the native cost is forced toward the unique J-cost $J(x)=(x+x^{-1})/2-1$ (T5); orientation globalization on prime axes is part of closing that uniqueness. Equating the two distinguished-axis halves keeps the blocker ledger coherent without duplicating refutation work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.