PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_not_iff_distinct_prime_pair_witness_character
plain-language theorem explainer
Negation of the one-sided target that prime calibration forces identity on the orbit-2 axis whenever it holds on any calibrated prime axis is equivalent to existence of a prime-calibrated ratio character witnessing a mixed branch on two distinct native primes. Cost-uniqueness and foundation auditors cite this bridge. The proof is a two-direction constructor transporting an existing uniformity-target equivalence through the identity-forces-two iff.
Claim. The following are equivalent: (i) it is not the case that every prime-direction-calibrated ratio character which is the identity on some calibrated prime axis is forced to be the identity on the orbit-$2$ prime axis; (ii) there exists a prime-direction-calibrated ratio character that witnesses a mixed branch between two distinct native prime orbits.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ assign to each ratio orbit either the identity or reciprocal branch. Prime-direction calibration restricts how $\chi$ may act on native prime axes. The one-sided distinguished-axis target asserts that, under calibration, identity on any calibrated prime axis forces identity on the orbit-$2$ axis.
The opposing model is a calibrated distinct-axis mixed-prime pair witness: a character that is prime-calibrated yet places a mixed (identity/reciprocal) pair on two different native primes. An upstream theorem already equates the negation of the related branch-uniformity target with existence of such a witness. A second upstream result identifies the branch-uniformity target with the forces-two identity target via a short iff chain.
This module develops native-cost uniqueness for PRC characters; the present statement is the forces-two form of the mixed-pair obstruction.
proof idea
Term-mode constructor on the biconditional. Left-to-right: from $\neg$ forces-two, compose with the mp direction of the uniformity $\leftrightarrow$ forces-two iff to obtain $\neg$ uniformity, then apply the mp of the upstream uniformity-not-iff-distinct-witness theorem. Right-to-left: from a distinct mixed-pair witness and a forces-two hypothesis, feed the witness into the mpr of the uniformity-not-iff theorem and the forces-two hypothesis into the mpr of the uniformity $\leftrightarrow$ forces-two iff, yielding the contradiction. No new arithmetic; pure Prop transport.
why it matters
Closes the forces-two packaging of the mixed-pair obstruction inside native-cost uniqueness. Downstream it is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles the conditional universal-foundation certificate (kernel, real complete ordered field, trace logic). In the Recognition forcing chain this sits under uniqueness of the native cost before J-uniqueness (T5) and the RCL; ruling out mixed prime branches is part of forcing a single global character, which later pins $J(x)=(x+x^{-1})/2-1$. Without the equivalence, the certificate could not swap freely between the uniformity and forces-two formulations of the same obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.