PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget_iff_split
plain-language theorem explainer
Prime calibration forbidding mixed nonunit witnesses is equivalent to the split package: no mixed prime witnesses, plus prime-witness control of all nonunit witnesses. Anyone tracking the native-cost uniqueness blocker or its refutation path cites this bridge. The proof is a two-constructor term packing the two directed lemmas.
Claim. The following are equivalent: (i) every prime-direction-calibrated ratio character has no mixed nonunit witnesses (no coexistence of an identity-oriented nonunit witness with a reciprocal-oriented nonunit witness); (ii) every such character has no mixed prime witnesses, and prime-witness control extends to arbitrary nonunit witnesses.
background
In the Primitive Recognition Calculus native-cost uniqueness module, ratio characters $\chi$ on ratio orbits are the algebraic carriers of cost data. Prime-direction calibration orients $\chi$ on primes. A nonunit witness is a non-unit orbit where the character records a one-sided orientation (identity-facing or reciprocal-facing). The no-mixed-witness target asserts that prime calibration forbids any character from carrying both orientations at once among nonunits.
The split target factors that claim into two pieces: first, rule out mixed witnesses already at the prime level; second, prove that control of prime witnesses propagates to composite nonunits. The module treats the split as the working form of the blocker while the existential nonunit form is the global statement.
Upstream, the two directed lemmas already exist: one derives the split package from the global nonunit target, and the other rebuilds the global target from the split by applying prime control after the no-mixed-prime half.
proof idea
Term-mode Iff introduction. The forward direction is the existing lemma that turns a global nonunit no-mixed-witness hypothesis into the conjunction of no-mixed-prime witnesses and prime-to-nonunit control. The reverse direction is the existing lemma that, given the split package, feeds the no-mixed-prime half into the prime-control half to recover the global nonunit target. No new algebra is performed here.
why it matters
This equivalence is the hinge between the global no-mixed-witness blocker and its split working form. Downstream, the split target is refuted by transporting a refutation of the global target across the reverse direction of this iff. That refutation feeds the native-cost uniqueness blocker certificate, which records which factorization and witness targets survive or fail under zero calibration. The same package is referenced from the conditional universal-foundation certificate, so the bridge sits on the path that decides how much of native-cost uniqueness can be promoted into the universal foundation layer. In the broader Recognition forcing chain this is local scaffolding hygiene around cost uniqueness, not a T5–T8 landmark, but it closes the bookkeeping that lets the uniqueness blocker be stated once and used in both global and split shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.