PRCPrimeCalibratedMixedPrimePairWitnessCharacter
plain-language theorem explainer
Packages the fully unpacked calibrated mixed-prime obstruction: existence of a ratio-orbit map that is a unit-multiplicative character, J-calibrated on every native prime direction, and carries a pair of mixed-prime branch witnesses. Downstream uniqueness lemmas cite it to split same-axis versus distinct-prime cases. Pure definitional conjunction of three named Props; no proof content.
Claim. There exists a map $\chi$ on rational orbits such that $\chi$ is a ratio character (preserves the unit and is multiplicative up to cross-equivalence), $\chi$ is prime-direction calibrated (the cost it induces agrees with canonical $J$-cost on every native prime orbit), and $\chi$ admits a mixed-prime pair of branch witnesses (named native primes $p$ and $r$, one identity-oriented and one reciprocal-oriented under cross-equivalence).
background
In the Primitive Recognition Calculus, costs on rational orbits are candidates for the unique native cost forced by the Recognition Composition Law. A ratio character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ is a quotient-native stand-in for a d'Alembert factor: it fixes the unit orbit and is multiplicative up to cross-equivalence rather than definitional equality.
Prime-direction calibration demands that the cost reconstructed from $\chi$ match the canonical $J$-cost $J(x)=(x+x^{-1})/2-1$ on every native prime orbit. The mixed-prime pair witness package then asserts two named prime axes $p$ and $r$ on which the character acts as identity and reciprocal respectively (cross-equality), removing the last propositional wrapper around the two branch witnesses.
Local setting is native-cost uniqueness: classify characters compatible with the PRC cost axioms and isolate residual mixed-prime configurations that still obstruct uniqueness.
proof idea
Definitional packaging only. The body is a single existential over maps $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ conjoined with the three Props: ratio-character axioms, prime-direction calibration, and the pair-packaged mixed-prime witnesses. No tactics, no lemmas applied.
why it matters
This is the current obstruction form with no remaining propositional packaging around the two branch witnesses (doc-comment). It sits on the path to native $J$-cost uniqueness (forcing-chain T5 / RCL uniqueness of $J$).
Downstream, the same-or-distinct equivalence splits it into a same-prime mixed pair versus a distinct-prime mixed pair, and conversion lemmas lift older mixed-witness packages into this form. Parent results include the iff with the same-or-distinct disjunction and the one-way introductions from same, distinct, and legacy mixed-witness characters. Closing either branch would shrink the residual obstruction toward uniqueness of the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.