PRCPrimeCalibrationForcesOrbitProductDisplayCompatibilityTarget
plain-language theorem explainer
Defines the target proposition that every ratio-orbit character which is a PRC ratio character and is calibrated on prime directions must be compatible with native orbit-product display. Cost-uniqueness and d'Alembert factorization work cites this as the missing quotient-respect step. The body is a pure Prop abbreviation, not a proof; discharge lives in the sibling `_proved` theorem.
Claim. The following is asserted as a target: for every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is a ratio character (unit and multiplicative up to cross-equivalence) and is prime-direction calibrated (its generated cost matches canonical $J$-cost on every prime orbit), then $\chi$ is orbit-product display compatible (its value on a product orbit equals its value on the ratio product of the factor orbits).
background
In the Primitive Recognition Calculus, costs are recovered from ratio-orbit characters via a d'Alembert-style factorization. A RatioOrbit is a rational display: signed numerator orbit over a nonzero distinction-nat denominator. A PRC ratio character is a map $\chi$ on those orbits that fixes the unit and is multiplicative, both only up to cross-equivalence, so the interface stays quotient-native.
Prime-direction calibration asks that the cost generated from $\chi$ agree with the canonical $J$-cost on every prime orbit direction. Separately, orbit-product display compatibility asks that $\chi$ on a product orbit equal $\chi$ on the ratio product of the factors. Upstream docs stress this is "not automatic from cross-equivalence; it is the quotient-respect step missing from the bare character interface."
The local module packages native-cost uniqueness targets. This definition names the claim that prime calibration alone should force that missing product-display step.
proof idea
No proof: this is a def equating a name to a universal Prop. The body quantifies over maps $\chi : \mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$, assumes the ratio-character structure and prime-direction calibration, and concludes orbit-product display compatibility.
Discharge is external. The sibling theorem ...Target_of_crossEq_respect reduces the target to a stronger cross-equivalence-respect hypothesis, then applies PRCCharacterOrbitProductDisplayCompatible_of_crossEq_respect. The closed form ...Target_proved feeds in the already-proved crossEq-respect target.
why it matters
Native cost uniqueness needs characters that are not merely multiplicative on representatives but respect the native display of orbit products. This target isolates that obligation under the economically natural hypothesis of prime calibration (agreement with $J$ on primes), tying into the T5 $J$-uniqueness landmark and the Recognition Composition Law route to a unique cost.
Downstream, PRCNativeCostUniquenessBlockerCertificate records Pass-25 status by splitting unfinished uniqueness work into exact Lean targets; this name is one of those pins. The framework has already closed the pin: PRCPrimeCalibrationForcesOrbitProductDisplayCompatibilityTarget_proved proves the Prop, so the blocker path no longer treats product-display compatibility under prime calibration as open mathematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.