PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter_of_non_two_mixed
plain-language theorem explainer
A calibrated mixed character with reciprocal orientation on the orbit-2 prime axis and identity orientation on some other native prime already supplies a distinct-axis mixed-prime pair witness. Anyone chasing character rigidity or branch-uniformity under prime calibration cites this reduction. The proof is a short existential repackaging: unpack the mixed model and insert the two-orbit as the second prime axis.
Claim. If there exists a ratio-orbit character $\chi$ that is prime-direction calibrated and mixed in the sharpened sense that the orbit-$2$ prime axis is reciprocal while some native prime $p\neq 2$ is identity-oriented, then there exists a prime-direction calibrated character witnessing a mixed branch between two distinct native prime orbits.
background
In the Primitive Recognition Calculus, ratio-orbit characters assign to each orbit an orientation (identity versus reciprocal) compatible with the cost automorphism structure. Prime-direction calibration restricts that assignment on native prime axes. The reciprocal map is the inversion automorphism on positive ratios (and the corresponding ledger event that swaps source and target with inverted ratio).
The hypothesis packages a sharpened mixed model: $\chi$ is a ratio character, prime-calibrated, with the two-step orbit reciprocal and some non-$2$ native prime identity-oriented. The conclusion weakens the geometric packaging only: it asks for a mixed pair of distinct native prime orbits, without forcing one of them to be the two-orbit in the statement of the model.
Locally this sits in the native-cost uniqueness development, where mixed characters are the obstruction branch against forcing uniform identity orientation on all prime axes.
proof idea
Tactic proof by existential destruction and reconstruction. Unpack the hypothesis into a character $\chi$, the ratio-character and prime-calibration witnesses, the two-prime reciprocal identity, and a non-$2$ prime $p$ with its identity orientation.
Rebuild the distinct-pair witness with the same $\chi$ and calibration data, taking $p$ as one prime axis and twoOrbit as the other. Discharge primality of the two-orbit via twoOrbit_primeOrbit, keep $p\neq 2$, keep the identity datum on $p$, and rewrite the reciprocal datum on the two-axis through twoPrimeDirection with simpa.
why it matters
This is the bridge from the sharpened two-adic mixed model to the generic distinct-axis mixed-pair model used by the rigidity cascade. Downstream, PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_not_of_non_two_mixed_character applies it to show that any such mixed character refutes the prime-identity branch-uniformity target: calibration cannot force every native prime axis to the identity orientation once a reciprocal two-axis and an identity non-two prime coexist.
It also feeds the conditional universal-foundation certificate in UniversalFoundation, which aggregates kernel, ordered-field, and trace-logic passes. In the broader Recognition forcing chain this is bookkeeping inside native J-cost uniqueness (the T5 J-uniqueness lane), not a new physical constant, but it closes a packaging gap so mixed-branch refutations can be stated uniformly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.