PRCPrimeCalibrationForcesOrbitProductDisplayCompatibilityTarget_of_crossEq_respect
plain-language theorem explainer
If prime calibration forces every ratio character to respect cross-equivalence of orbits, then it also forces product-display compatibility. Native-cost uniqueness arguments cite this as the bridge from the sharper cross-eq target to the product-display target. The proof is a short term reduction: instantiate the hypothesis and apply the character-level cross-eq-to-product lemma.
Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated respects ratio cross-equivalence. Then every such $\chi$ is product-display compatible: it identifies product orbit directions with the ratio products of the corresponding factor directions.
background
In the Primitive Recognition Calculus, ratio orbits are the native carriers of multiplicative structure, and a ratio character $\chi$ maps orbits to orbits while preserving the character axioms. Prime-direction calibration pins how $\chi$ acts on prime orbit directions. Cross-equivalence is the quotient relation that makes two ratio presentations the same orbit; a character that respects it is genuinely quotient-native.
Product-display compatibility is the structural demand that $\chi$ treat a product orbit direction as the ratio product of the factor directions. The module packages two calibration targets: a sharper one (prime calibration forces cross-eq respect) and a coarser one (prime calibration forces product-display compatibility). Upstream, the character-level lemma already shows that any character respecting cross-equivalence is automatically product-display compatible.
proof idea
Term-mode reduction. Introduce a character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the assumed calibration-forces-cross-eq target at $(\chi,h_\chi,h_{\mathrm{prime}})$ to obtain cross-eq respect, then feed that into the upstream lemma that cross-eq respect implies product-display compatibility. No extra algebraic work.
why it matters
Closes the implication from the sharper cross-eq calibration target to the product-display target used in native-cost uniqueness. Downstream, the proved form of the product-display target is exactly this theorem applied to the proved cross-eq target, and that proved form feeds the native-cost uniqueness blocker certificate. In the Recognition forcing picture this is bookkeeping on the character side of the native cost (the J-cost lineage), ensuring calibrated characters respect the multiplicative display needed before uniqueness of the cost functional can be certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.