PRCPrimeCalibratedMixedPrimeWitnessesCharacter
plain-language theorem explainer
Names the obstruction proposition: there exists a ratio-orbit character that is prime-direction calibrated and still carries both an identity-oriented and a reciprocal-oriented prime witness. Anyone proving native cost uniqueness or discharging the no-mixed-prime blocker cites this packing. The body is a pure existential conjunction of three character properties; no proof work lives here.
Claim. There exists a map $\chi$ on ratio orbits such that $\chi$ is a ratio character, $\chi$ is prime-direction calibrated, and $\chi$ admits mixed prime witnesses (both an identity-oriented prime axis and a reciprocal-oriented prime axis).
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). A ratio character is a structure-preserving map on those orbits; cost is recovered from the character via the native doubled-trace / J-cost pipeline.
Prime-direction calibration forces the character's action on named prime axes to match the ledger's identity and reciprocal orientations (identity sits at the J-cost minimum $x=1$; reciprocal swaps source/target and inverts the ratio). Mixed-prime witnesses mean the same calibrated character still supports one prime axis identity-oriented and another reciprocal-oriented.
This module packages native-cost uniqueness blockers as named Props. The present definition is the calibrated mixed-prime witness model; its nonexistence is definitionally the current no-mixed-prime witness blocker.
proof idea
Definitional packing only: the proposition is the existential
$\exists,\chi$, with three conjuncts (ratio character, prime-direction calibration, mixed-prime witnesses). No tactics, no lemmas applied. Downstream theorems unpack or repack this triple via rcases / exact \langle\chi, \ldots\rangle and the bridge lemmas between mixed-witness and mixed-pair-witness forms.
why it matters
This is the named obstruction in the PRC native-cost uniqueness chain. Nonexistence of the model is the no-mixed-prime witness blocker; several parent results treat it as the positive witness side of that dichotomy.
Downstream: absurdity from the no-mixed target (..._absurd_of_no_mixed_prime_witnesses); classical recovery from failure of the no-mixed or prime-pair product-cost targets; and the iff with the fully unpacked pair-witness character (named native primes $p$ identity-oriented and $r$ reciprocal-oriented, "current obstruction with no remaining propositional packaging").
In the broader RS forcing picture this sits under native J-cost uniqueness (T5 / RCL territory): mixed identity/reciprocal prime axes would break the single calibrated cost character the ledger needs. Closing the blocker means proving this Prop false under the native hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.