PRCPrimeCalibrationForcesNonunitNoMixedWitnessesSplitTarget
plain-language theorem explainer
Conjunction that packages the no-mixed-witness blocker as two successive obligations: rule out mixed prime witnesses under prime-direction calibration, then lift prime-witness control to arbitrary nonunit composites. Native-cost uniqueness certificates and the split/iff lemmas cite it as the intermediate target shape. Pure definitional ∧ of two Prop targets; no proof content.
Claim. The split no-mixed-witness target is the conjunction of (i) every prime-direction-calibrated ratio character has no mixed prime witnesses, and (ii) under the same hypotheses, prime-witness control extends to nonunit composite witnesses.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes a candidate cost orientation. Prime-direction calibration fixes how $\chi$ treats prime generators; mixed witnesses are orientations that flip inconsistently across prime factors. The first conjunct is the existential prime-witness form of no-mixed prime orientation: for every ratio character that is a PRC ratio character and prime-direction calibrated, the no-mixed-prime-witnesses predicate holds.
The second conjunct is the composite bridge: under the same character and calibration hypotheses, the prime no-mixing property is required to control arbitrary nonunit no-mixing (prime witnesses control nonunit witnesses). The local module is native cost uniqueness for PRC; the split isolates local orientation from one-sided witness exclusion as the staged form of witness globalization.
proof idea
Definitional abbreviation only: the target is literally the conjunction of the no-mixed-prime-witnesses target and the prime-witnesses-control-nonunit-witnesses target. No tactics, no lemmas applied at the definition site. Downstream constructors build inhabitants by pairing a proof of the first conjunct with a proof of the second (or derive the pair from the unsplit nonunit target via the recorded iff).
why it matters
This is the staged form of the current no-mixed-witness blocker inside native cost uniqueness. It feeds PRCNativeCostUniquenessBlockerCertificate, which records that uniqueness is not closed but the missing mathematics is split into exact Lean targets. The iff with the unsplit nonunit no-mixed-witnesses target, the two introduction lemmas (from prime side / from nonunit side), and the of-split elimination lemma all route through this Prop.
It also appears among universal-foundation open targets. Framework-wise it sits under J-cost uniqueness (T5) and the Recognition Composition Law path: native cost must be forced as the unique character-compatible cost, and witness globalization is one of the remaining blockers. Notably a later theorem refutes the split target, so the certificate path treats this obligation as closed negatively rather than as an open proof debt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.