PRCCharacterOrbitProductDisplayCompatible
plain-language theorem explainer
A ratio character is product-display compatible when its value on a product orbit agrees, under cross-equivalence, with its value on the ratio product of the factor orbits. Anyone deriving native PRC cost uniqueness from character axioms cites this interface condition. The declaration is a Prop definition packaging the multiplicative quotient-respect step missing from a bare RatioOrbit map; it is not automatic from cross-equivalence alone.
Claim. A map $\chi$ from ratio orbits to ratio orbits is product-display compatible if, whenever nonzero distinction naturals $a$, $b$, and $p$ satisfy $a\cdot b=p$, one has $\chi(\mathrm{dir}(p))\sim\chi(\mathrm{dir}(a)\cdot\mathrm{dir}(b))$, where $\sim$ denotes cross-multiplication equivalence of ratio orbits and $\mathrm{dir}$ sends a nonzero distinction natural to its directed ratio orbit.
background
In the Primitive Recognition Calculus, rationals are rebuilt as ratio orbits: pairs of signed $\delta$-orbits with a native cross-multiplication relation. Upstream, crossEq says two ratio orbits are equivalent when $a.\mathrm{num}\cdot b.\mathrm{den}$ balances $b.\mathrm{num}\cdot a.\mathrm{den}$ as signed orbits; that is the internal PRC stand-in for rational equality, defined entirely on orbit positions.
A raw map $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ is the working form of a PRC character before quotient descent. Multiplicative structure on distinction naturals lifts to directed orbits via orbitDirection and ratio-orbit multiplication. Agreement of $\chi$ on a product orbit with $\chi$ on the product of factor orbits is a separate respect condition: the character must not see a different display of the same multiplicative fact.
This module develops native-cost uniqueness from character hypotheses (trace matching, d'Alembert structure, prime-local orientation). Product-display compatibility is the multiplicative half of making a bare character usable as a quotient-native object.
proof idea
Definition only: the body is the universal property itself. For all nonzero distinction naturals $a,b,p$ with $a\cdot b=p$, require cross-equivalence between $\chi$ on the directed orbit of $p$ and $\chi$ on the ratio-orbit product of the directed orbits of $a$ and $b$. No lemmas are applied; downstream theorems take the Prop as a named hypothesis.
why it matters
Native cost uniqueness needs characters that respect how products are displayed, not only pointwise cross-equivalence. This Prop is the missing multiplicative quotient-respect step on the bare character interface, and it is threaded through the prime-to-composite lifting arguments in the same module.
Downstream it is a hypothesis of the prime-local reflection theorems (mixed and pure nonunit identity/reciprocal witnesses reflecting prime witnesses), of the all-prime-identity and all-prime-reciprocal orbit theorems, and of the comparable-trace respect lemmas for nonunit identity. Those results assemble the character into a globally coherent multiplicative object before cost is recovered from doubled trace.
In the broader forcing chain this sits under T5 J-uniqueness: the native cost is forced to be the J-cost once character axioms (including product-display compatibility) pin the doubled-trace d'Alembert structure. Without this condition, a map could scramble factorizations while still looking like a character on primes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.