PRCPrimeCalibrationForcesPrimeWitnessesControlNonunitWitnessesTarget
plain-language theorem explainer
Packages the open-style target that every prime-calibrated ratio character has prime no-mixing controlling arbitrary nonunit no-mixing. Cited by the native-cost uniqueness blocker split and by the proved discharge of this target. Body is a pure Prop abbreviation: universal quantification over characters with the two hypotheses and the composite bridge conclusion.
Claim. For every map $\chi$ on ratio orbits that is a ratio character and is calibrated on every native prime direction (generated cost matches canonical $J$-cost on each prime orbit), prime no-mixing for $\chi$ implies nonunit no-mixing for $\chi$.
background
In the Primitive Recognition Calculus, costs are studied via ratio characters: maps $\chi$ on ratio orbits (signed numerator over nonzero distinction denominator) that fix the unit and are multiplicative up to cross-equivalence. Cross-equivalence keeps the statements quotient-native rather than definitionally equal.
Prime-direction calibration means that the cost generated from $\chi$ agrees with the canonical $J$-cost on every prime orbit direction. The composite bridge property then says: if $\chi$ has no mixed prime witnesses, it has no mixed nonunit witnesses. That is the exact remaining link after prime witnesses are isolated.
This module packages uniqueness obstacles for native PRC cost as named Lean targets. The present definition is the quantified form of that composite bridge under the standing character and calibration hypotheses.
proof idea
Definitional packaging only: the body is the universal statement $\forall,\chi,;\mathrm{PRCRatioCharacter},\chi\to\mathrm{PrimeDirectionCalibrated},\chi\to\mathrm{PrimeWitnessesControlNonunitWitnesses},\chi$. No tactics or lemmas are applied at this site. Discharge lives downstream, via the reflection form (mixed nonunit witnesses reflect to mixed prime-axis witnesses) and the proved theorem that instantiates that path.
why it matters
This is one half of the split no-mixed-witness blocker: the conjunction of "no mixed prime witnesses under prime calibration" with this control target. It feeds PRCNativeCostUniquenessBlockerCertificate, which records that native cost uniqueness is not fully closed but is split into exact Lean targets.
Downstream, the target is equivalent to its reflection form and is already discharged: the _proved theorem obtains it from the proved mixed-nonunit-reflects-prime target. In the Recognition forcing picture this sits under native $J$-cost uniqueness (T5 lineage): characters calibrated on primes must not admit mixed nonunit witnesses that would spoil unique d'Alembert factorization into the canonical cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.