PRCPrimeCalibrationForcesCharacterCrossEqRespectTarget
plain-language theorem explainer
Prime calibration of a ratio character is proposed to force quotient-respect: any ratio-orbit map that is a PRC character and agrees with canonical J-cost on every prime direction must send cross-equivalent displays to cross-equivalent values. Cost-uniqueness and product-display arguments cite this Prop as the missing setoid condition. The declaration is a pure Prop target; discharge is by later uniqueness of reduced sign-canonical ratios.
Claim. For every map $\chi$ from ratio-orbit displays to ratio-orbit displays, if $\chi$ is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is prime-direction calibrated (its generated cost matches canonical $J$-cost on every prime orbit), then $\chi$ respects cross-equivalence: cross-equivalent inputs yield cross-equivalent outputs.
background
In the Primitive Recognition Calculus, costs and characters are stated on ratio-orbit displays rather than bare rationals. A RatioOrbit is an integer numerator over a nonzero orbit denominator (K4.7). Cross-equivalence identifies displays that represent the same rational ratio, so maps used as characters must respect that relation to be quotient-native.
A ratio character is a map $\chi$ that fixes the unit orbit and is multiplicative up to cross-equivalence; it is the candidate factor in a d'Alembert factorization of a PRC cost. Prime-direction calibration asks that the cost generated from $\chi$ agree with the canonical $J$-cost on every prime orbit direction. Quotient-respect (PRCCharacterRespectsCrossEq) is the setoid condition: equivalent displays receive equivalent character values.
This module packages native-cost uniqueness into exact Lean targets. The present definition isolates the claim that prime calibration alone should already force quotient-respect, without a separate ad-hoc hypothesis on $\chi$.
proof idea
No proof body: the declaration is a Prop abbreviation packaging a universal implication. Downstream discharge routes through reduced sign-canonical uniqueness. One path assumes a normalize-ratio canonical target and applies the lemma that every ratio character then respects cross-equivalence (prime calibration is unused in that branch). Another reduces the reduced-sign-canonical uniqueness target to the normalize-ratio target, then reuses the same argument. A proved theorem closes the chain by supplying the uniqueness hypothesis. A separate downstream lemma turns the present target into orbit product-display compatibility by applying the cross-equivalence respect conclusion to each character.
why it matters
Without quotient-respect, a raw map on ratio orbits is not yet a quotient-native PRC character, so product-display compatibility and native-cost uniqueness cannot close. The doc-comment frames this Prop as the sharper source of that compatibility: prime calibration should force cross-equivalence respect.
Downstream, the native-cost uniqueness blocker certificate lists exact missing mathematics; this target feeds the product no-mixing / orbit product-display compatibility target via the of-crossEq-respect theorem. Sibling proved theorems already discharge the Prop under reduced sign-canonical uniqueness, so the blocker path can treat cross-equivalence respect as settled once that uniqueness is in hand.
In the broader Recognition forcing chain this sits under native $J$-cost uniqueness (T5 landmark: $J(x)=(x+x^{-1})/2-1$), ensuring character factorizations stay on the quotient of ratio displays rather than on presentation-dependent data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.