PRCPrimeCalibrationForcesNonunitNoMixedWitnessesTarget
plain-language theorem explainer
Prime calibration of a ratio character forces the existential nonunit no-mixed-witness property: identity-oriented and reciprocal-oriented nonunit witnesses cannot coexist. Anyone closing native cost uniqueness via the witness-split bridge cites this Prop target. It is a packaged universal statement, not a proved theorem.
Claim. For every map $\chi$ from ratio orbits to ratio orbits that is a ratio character (unit at one, multiplicative under cross-equivalence) and is prime-direction calibrated (its generated cost matches canonical $J$-cost on every prime orbit), $\chi$ admits no mixed nonunit witnesses: there cannot simultaneously exist an identity-oriented nonunit witness and a reciprocal-oriented nonunit witness.
background
In the Primitive Recognition Calculus, costs on rational orbits are factored through ratio characters. A ratio character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ is a quotient-native candidate for d'Alembert factorization: it fixes the unit orbit under cross-equivalence and is multiplicative for orbit multiplication. Ratio orbits themselves are signed-numerator over nonzero distinction-denominator displays of rational scale.
Prime-direction calibration means that the cost reconstructed from $\chi$ agrees, again under cross-equivalence, with the canonical $J$-cost on every prime orbit direction. The $J$-cost is the unique cost forced by the Recognition Composition Law (T5: $J(x)=(x+x^{-1})/2-1$).
The nonunit no-mixed-witnesses property is the existential branch-coupling ban: one cannot have both an identity-oriented nonunit witness and a reciprocal-oriented nonunit witness for the same character. This module packages that implication under prime calibration as an explicit Prop target.
proof idea
Definitional packaging only. The body is the universal Prop $\forall\chi,;\mathrm{PRCRatioCharacter},\chi\to\mathrm{PRCCharacterPrimeDirectionCalibrated},\chi\to\mathrm{PRCCharacterNonunitNoMixedWitnesses},\chi$. No tactics, no lemmas applied; the three named predicates are the upstream interfaces being composed into a single target.
why it matters
This target is the composite bridge for the witness split: under prime calibration, forbidding mixed nonunit witnesses is the strong form that should control prime-only no-mixing and the identity-excludes-reciprocal form. Downstream, it feeds the Pass-25 blocker certificate for native cost uniqueness, and is related by proved iff and of-lemmas to the no-mixed-prime-witnesses target, the identity-witness-excludes-reciprocal target, and the split target.
Native cost uniqueness is the PRC route to forcing the unique $J$-cost (forcing-chain T5). Closing this target would discharge one exact Lean hole in that uniqueness program; until then it remains an open mathematical obligation recorded as a named Prop rather than a theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.