PRCPrimeCalibratedDistinctPrimeMixedPairWitnessCharacter
plain-language theorem explainer
Packages the existence of a ratio character that is a d'Alembert factorization candidate, agrees with canonical J-cost on every native prime direction, and places identity-oriented and reciprocal-oriented prime witnesses on two different prime orbits. Cited wherever the mixed-prime branch is split into same-axis versus distinct-axis cases under prime calibration. Pure definitional packaging of three conjuncts; no proof content.
Claim. There exists a map $\chi$ on ratio orbits such that $\chi$ is a ratio character (unit-preserving and multiplicative up to cross-equivalence), the cost generated by $\chi$ agrees with canonical $J$-cost on every native prime direction, and the identity-oriented and reciprocal-oriented prime witnesses for $\chi$ live on two distinct native prime orbits.
background
In the primitive recognition calculus, costs are studied via ratio characters: maps $\chi$ on ratio orbits (rational displays with signed-orbit numerator and nonzero distinction-nat denominator) that preserve the unit and multiply up to cross-equivalence. Cross-equivalence is the quotient-native equality used throughout, so statements stay well-defined on orbits rather than raw representatives.
Prime-direction calibration requires that the cost generated from $\chi$ match the canonical $J$-cost on every native prime orbit direction. Distinct-axis mixed-prime pair witnesses assert that the identity-oriented and reciprocal-oriented prime witnesses sit on two different native primes $p \neq r$, each with the appropriate cross-equivalence conditions.
This module develops uniqueness of the native PRC cost under d'Alembert-type factorization hypotheses. The present definition is the calibrated distinct-axis branch of that case analysis.
proof idea
Definitional abbreviation only: the proposition is the existential package of three already-named predicates on a single map $\chi$ (ratio character, prime-direction calibration, and distinct-prime mixed-pair witnesses). No tactics, no lemmas applied.
why it matters
Splits the calibrated mixed-prime-pair case into same-axis versus distinct-axis subcases. Downstream, the mixed-pair character is equivalent to the disjunction of the same-prime and distinct-prime packages, and the distinct package injects into the mixed package. A uniformity theorem then shows prime calibration plus identity-branch uniformity rules the distinct package out entirely: $\neg$ of this proposition follows from the prime-identity branch uniformity target.
That exclusion is part of forcing the native cost toward the unique $J$-cost of the Recognition Composition Law (T5: $J(x)=(x+x^{-1})/2-1$). Closing off distinct-axis mixed witnesses under calibration narrows the residual character models that could still compete with $J$ on the prime ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.