PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_refuted
plain-language theorem explainer
The orbit-2 reciprocal mixed-witness exclusion target is false: prime-direction calibration of a ratio character does not force reciprocal orientation on the prime-2 axis to exclude every identity-oriented native prime witness. Native-cost uniqueness and the next exclusion-target refutation cite this. The proof is a one-line transfer across an equivalence onto the already-refuted mixed-composite cost-consistency target.
Claim. It is not the case that every prime-direction-calibrated ratio character $\chi$ satisfies the orbit-$2$ mixed-witness exclusion: reciprocal orientation of the prime-$2$ axis need not rule out every identity-oriented native prime witness.
background
In the Primitive Recognition Calculus, cost uniqueness is attacked through ratio characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ that obey the PRC ratio-character axioms and a prime-direction calibration condition. Calibration fixes how prime axes sit relative to the reciprocal versus identity orientations that generate native prime witnesses.
The target proposition asserts a two-specific rigidity claim: once $\chi$ is a calibrated ratio character and the orbit-$2$ prime axis is reciprocal-oriented, no identity-oriented native prime witness is allowed. An in-module equivalence identifies that exclusion target with a mixed-composite cost-consistency target (a statement about cost values on mixed composite orbits built from the same calibration data).
Upstream, the mixed-composite consistency target is already refuted by reduction to a prime-pair product cost-consistency refutation. The present declaration simply closes the corresponding witness-exclusion form.
proof idea
Term-mode one-liner. Assume the witness-exclusion target htarget. Apply the forward direction of the in-module equivalence
PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_mixed_composite_cost_consistency
to obtain the mixed-composite cost-consistency target, then discharge by the already-proved refutation
PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_refuted. No new arithmetic is performed.
why it matters
This clears one concrete false forcing claim on the native-cost uniqueness path. Downstream it is consumed by PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityTarget_refuted (the non-witness form of the same exclusion) and by prc_native_cost_uniqueness_blocker_certificate, which packages proved and refuted factorization targets into a single blocker certificate. That certificate in turn feeds prc_universal_foundation_conditional_certificate in UniversalFoundation.
In the broader RS picture the work sits under T5 J-uniqueness: native cost is meant to be forced to the J-cost $J(x)=(x+x^{-1})/2-1$ by character and calibration constraints. Refuting over-strong mixed-witness exclusions prevents a spurious rigidity route and keeps the uniqueness argument honest about which prime-axis orientations are actually forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.