PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_iff_two_prime_reciprocal_excludes_witness
plain-language theorem explainer
Under prime-direction calibration of a ratio character, forcing identity on the orbit-2 prime axis from identity on any calibrated prime axis is equivalent to excluding any identity-oriented native prime witness once the orbit-2 axis is reciprocal. Native-cost uniqueness and the universal-foundation certificate cite this bridge. The proof is a pure Iff constructor pairing the two already-proved one-sided implications.
Claim. The following two targets are equivalent. (A) For every ratio character $\chi$ that is prime-direction calibrated, identity of $\chi$ on any calibrated prime axis forces identity of $\chi$ on the orbit-$2$ prime axis. (B) For every such $\chi$, if the orbit-$2$ prime axis is reciprocal-oriented, then no identity-oriented native prime witness exists.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how a candidate native cost orients each prime axis (identity versus reciprocal). Prime-direction calibration restricts $\chi$ so that its action on calibrated primes is coherent with the native cost hypotheses.
The first target is the one-sided distinguished-axis statement: once any calibrated prime sits on the identity branch, the orbit-$2$ prime axis must also sit on identity. The second target is the two-specific mixed-witness exclusion: if orbit $2$ is reciprocal, no native prime may remain identity-oriented. Both live in the native-cost uniqueness module, which aims to force the J-cost $J(x)=(x+x^{-1})/2-1$ as the unique admissible cost (T5 in the forcing chain).
Upstream, each direction of the equivalence is already a theorem: identity-forces-two implies the reciprocal-excludes-witness target, and conversely the witness-exclusion target implies the identity-forces-two target (via the non-witness reciprocal-exclusion intermediate).
proof idea
Term-mode Iff introduction. The forward arrow is the existing lemma that turns the identity-forces-two target into the two-prime-reciprocal-excludes-witness target. The reverse arrow is the existing lemma that recovers identity-forces-two from the witness-exclusion target. No new algebraic work; the constructor simply packages the two one-sided maps.
why it matters
This equivalence is the hub of a long iff-chain that rewrites the distinguished-axis rigidity target into several concrete nonexistence statements: no two-prime mixed character, no non-two mixed character, no non-two composite defect character, no composite cost-defect character, and mixed-composite cost consistency. Downstream theorems obtain those forms by trans through this bridge.
It feeds prc_native_cost_uniqueness_blocker_certificate and, outside the module, prc_universal_foundation_conditional_certificate. In the Recognition framework that matters because native-cost uniqueness is the PRC route to J-uniqueness (T5) and the Recognition Composition Law; closing mixed-character loopholes on the orbit-2 axis is exactly the rigidity needed before the phi fixed point and eight-tick structure can be forced cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.