PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_mixed_composite_cost_consistency
plain-language theorem explainer
Equivalence of two prime-calibration targets: the mixed-witness exclusion (if orbit-2 is reciprocal-oriented, no identity-oriented native prime witness exists) and the mixed composite cost-consistency requirement (calibration forces cost agreement on composites 2·p under that mixed orientation). Used by the prime-identity forcing chain and the PRC universal-foundation certificate. Proof is a two-way constructor through the no-composite-cost-defect intermediate.
Claim. The mixed-witness exclusion target—if the orbit-$2$ prime axis is reciprocal-oriented, then no identity-oriented native prime witness may exist—is equivalent to the mixed composite cost-consistency target: under prime-direction calibration, whenever orbit $2$ is sent reciprocal and a distinct native prime $p$ is sent identity, the composite direction $2\cdot p$ must still be cost-calibrated.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns to each ratio orbit an oriented image orbit, subject to the PRC ratio-character axioms and prime-direction calibration. Orbit $2$ is special: its orientation (identity vs reciprocal) interacts with orientations of other native primes $p$ through composite directions $2\cdot p$.
The mixed-witness exclusion target asserts that a reciprocal orientation on orbit $2$ forbids any identity-oriented native prime witness. The mixed composite cost-consistency target is the cost-visible form of the same rigidity: even under that mixed orientation data, prime calibration must force cost agreement on the composite $2\cdot p$.
Both sit in the native-cost uniqueness module, which isolates which character orientations are compatible with the native cost (the J-cost lineage) before the universal foundation certificate assembles the kernel, ordered-field, and trace-logic pieces.
proof idea
Term-mode constructor on the biconditional.
Forward: from the exclusion target, apply the already-proved iff with nonexistence of the composite cost-defect character, then feed that nonexistence into ...MixedCompositeCostConsistencyTarget_of_no_composite_cost_defect.
Reverse: from cost-consistency, apply ...absurd_of_mixed_composite_consistency to obtain nonexistence of the defect character, then reverse the same iff to recover the exclusion target.
No new arithmetic; pure Prop-level chaining through the defect-character intermediate.
why it matters
Closes the bridge between the witness-exclusion formulation and the cost-consistency formulation of the orbit-$2$ mixed-orientation blocker. Downstream, it is the middle step of
...PrimeIdentityForcesTwoPrimeIdentityTarget_iff_mixed_composite_cost_consistency
and of
...MixedCompositeCostConsistencyTarget_iff_no_non_two_mixed_character,
and it is the transport used by
...ReciprocalExcludesPrimeIdentityWitnessTarget_refuted.
That refutation path feeds the conditional universal-foundation certificate in UniversalFoundation, so the equivalence is load-bearing for the PRC foundation stack rather than a local rewrite. In the broader RS forcing chain it sits under native-cost uniqueness for the J-cost (T5 lineage), before phi and dimensional forcing are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.