PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter
plain-language theorem explainer
Named proposition packing existence of a prime-calibrated ratio character that carries same-axis mixed-prime pair witnesses. Downstream uniqueness arguments cite it when splitting mixed-pair models into same-orbit versus distinct-orbit cases, and when discharging the same-orbit branch as absurd. The body is pure existential packaging of three character properties; no proof work lives here.
Claim. There exists a map $\chi$ from ratio orbits to ratio orbits such that $\chi$ is a ratio character (preserves the unit and is multiplicative up to cross-equivalence), $\chi$ is calibrated on every native prime direction (the cost it generates matches canonical $J$-cost on each prime orbit), and $\chi$ admits same-axis mixed-prime pair witnesses (identity-oriented and reciprocal-oriented prime witnesses carried by one and the same native prime orbit).
background
In the primitive recognition calculus, costs are analyzed through ratio characters: maps $\chi$ on ratio orbits (rational displays with signed-orbit numerator and nonzero distinction-nat denominator) that are unit-preserving and multiplicative up to cross-equivalence rather than definitional equality. The generated cost of such a character is compared to the canonical $J$-cost on orbits.
Prime-direction calibration requires that this generated cost agree with $J$ on every native prime orbit. Same-axis mixed-prime pair witnesses are the self-reciprocal branch-conflict case: both the identity-oriented and reciprocal-oriented prime witnesses live on a single native prime orbit (as opposed to two distinct primes).
This module builds native uniqueness of the recognition cost by forcing characters that match $J$ on primes to avoid mixed-pair witness configurations. The present definition isolates the same-orbit mixed branch under full prime calibration.
proof idea
Definitional packaging only. The proposition is the existential claim that some map $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ simultaneously satisfies the ratio-character axioms, prime-direction calibration (cost from $\chi$ cross-equals canonical $J$ on each prime direction), and the same-prime mixed-pair witness predicate. No tactics or lemmas are applied; downstream theorems unpack the triple conjunction.
why it matters
This is the same-orbit half of the calibrated mixed-prime pair model. Parent results use it to split the general mixed-pair character into same versus distinct cases (iff and introduction/elimination lemmas), then prove the same-orbit branch is absurd. That absurdity feeds the target that prime calibration forces no mixed-prime witnesses, and the related product-cost consistency target for prime pairs.
In the Recognition framework this sits inside native $J$-cost uniqueness for the primitive calculus: characters that reproduce $J$ on primes cannot host self-reciprocal mixed witnesses. That uniqueness underwrites the T5 $J$-form $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law at the orbit level. The companion distinct-axis model is the other disjunct; together they close the mixed-pair case analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.