PRCPrimeCalibrationForcesOrbitProductDisplayCompatibilityTarget_proved
plain-language theorem explainer
Prime calibration of a ratio-orbit character forces product-display compatibility: the character respects the native equality between product orbit directions and ratio products of factor directions. Cited by native-cost uniqueness and nonunit orientation/coherence lemmas. Proof is a one-line term applying the cross-equivalence-respect theorem through a reduction lemma.
Claim. For every map $\chi$ from ratio orbits to ratio orbits that is a ratio character and is prime-direction calibrated, $\chi$ is orbit-product-display compatible: it respects the native equality between product orbit directions and ratio products of the factor directions.
background
In the Primitive Recognition Calculus, ratio orbits carry the discrete multiplicative skeleton on which native cost is later read. A ratio character $\chi$ is a structure-preserving map on those orbits. Prime-direction calibration pins $\chi$ on prime generators so that its values match the preferred prime directions of the native display.
Product-display compatibility asks that $\chi$ respect the native identification of a product orbit direction with the ratio product of the factor directions. Without that, $\chi$ is not yet quotient-native on products, and later orientation and trace comparisons cannot propagate from primes to composite nonunits.
The sharper source is cross-equivalence respect: prime calibration should force the raw character to respect ratio cross-equivalence. The upstream proved target establishes that respect; the present target is the product-display form needed downstream.
proof idea
One-line term proof. Apply the reduction lemma that derives product-display compatibility from cross-equivalence respect, feeding it the already-proved prime-calibration-forces-cross-eq-respect theorem. That reduction intro's the character and the two hypotheses, then invokes the character-level lemma that cross-eq respect implies orbit-product-display compatibility.
why it matters
Closes the product-display compatibility target in the prime-calibration forcing chain inside PRC native-cost uniqueness. Downstream, mixed nonunit identity and reciprocal witness reflection, nonunit orbit product local orientation (via display-compatible no-mix), and related orientation-coherence targets all invoke this proved form. It also sits on the dependency path into the native-cost uniqueness blocker certificate.
In framework terms this is bookkeeping on the discrete side of J-cost uniqueness (T5): characters must act as true quotient maps on products before the doubled-trace d'Alembert structure can force the native cost shape. Without display compatibility, prime calibration would not globalize to composite orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.