PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_not_iff_distinct_prime_pair_witness_character
plain-language theorem explainer
Negation of the prime-calibration branch-uniformity target is equivalent to existence of a calibrated character with a mixed branch between two distinct native prime orbits. Anyone tracking the PRC native-cost uniqueness ladder cites this as the clean logical dual of the two one-way implications. The proof is a two-direction constructor that wires those implications together by contradiction.
Claim. The following are equivalent: (i) it is not the case that every prime-direction-calibrated ratio character is identity-branch-uniform on native prime axes; (ii) there exists a ratio character that is prime-direction calibrated and witnesses a mixed branch between two distinct native prime orbits.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters $\chi$ assign orbits to orbits and encode branch structure along native prime axes. Prime-direction calibration restricts how $\chi$ orients those axes. The branch-uniformity target asserts that every such calibrated character places all native prime axes on the identity branch whenever any identity-oriented native prime axis is present.
The opposing witness is existential: a calibrated character whose mixed branch joins two different native prime orbits. Upstream, one theorem shows that branch uniformity immediately rules out any such distinct-prime mixed-pair witness (by an absurdity lemma on mixed pairs under uniformity). The converse shows that absence of every such witness yields the full uniformity target, via a local no-distinct-pair reduction already available from the local prime-orientation target.
This declaration sits at the interface of those two one-way facts and packages them as a single classical equivalence between failure of the target and existence of the witness.
proof idea
Term-mode constructor on the biconditional.
Left-to-right: assume the uniformity target fails. Argue by contradiction that no distinct-prime mixed-pair witness exists; the upstream implication from no-witness to the uniformity target then restores the target, contradicting the assumption, so a witness must exist.
Right-to-left: assume a distinct-prime mixed-pair witness and assume the uniformity target. Feed the target into the upstream implication that uniformity forbids any such witness, and discharge the contradiction against the assumed witness.
why it matters
This equivalence is the hinge that lets later steps rewrite failure of prime-identity branch uniformity as a concrete mixed-pair obstruction. The immediate parent reuses it to obtain the analogous not-iff for the stronger two-prime-identity target, chaining the same witness character one level higher in the forcing ladder.
Downstream it also feeds the conditional universal-foundation certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic passes. Within Recognition Science this is scaffolding for native-cost uniqueness under prime calibration: ruling out mixed distinct-prime branches is part of forcing the unique J-cost structure (T5) and the self-similar $\phi$ fixed point (T6) once characters are constrained on the prime-axis graph. It does not itself close cost uniqueness; it only dualizes one intermediate target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.