PRCCharacterPrimePairProductCostConsistent
plain-language theorem explainer
A character χ of ratio orbits is prime-pair product cost consistent when, for every pair of native primes, the cost χ assigns to the product of their prime directions agrees with the native cost on that product (via cross-multiplication equality of orbits). Admissibility packages and native-cost uniqueness proofs cite this as a character-local field. It is a pure Prop definition, not a proved statement.
Claim. A map $\chi$ from ratio orbits to ratio orbits is prime-pair product cost consistent if, for every pair of prime distinction-natural numbers $p,r$ (with their prime-orbit witnesses), the cost induced by $\chi$ on the product of the corresponding prime directions is cross-multiplication equivalent to the native cost orbit of that same product.
background
In the Primitive Recognition Calculus, ratio orbits are the internal stand-in for positive rationals built from signed $\delta$-orbits. Two orbits are identified by crossEq when cross-multiplication balances their numerators and denominators as signed orbits (the PRC form of rational equality).
A ratio character $\chi$ is a map on ratio orbits used to induce a cost via costFromCharacter. Native cost on an orbit is the canonical display onRatioOrbit. Prime directions are the distinguished ratio-orbit axes attached to prime distinction-naturals. The module develops native-cost uniqueness: which characters can induce the recognition cost, and which admissibility fields rule out countermodels (notably two-adic valuation twists).
The related global target asks that prime calibration of any ratio character already force product-cost consistency on all prime pairs. The present definition is the character-local surface of that same condition, so it can sit as a field of an admissibility structure rather than as a universal implication.
proof idea
No proof: this is a Prop-valued definition. The body is a four-quantifier universal statement over prime orbits $p,r$ asserting crossEq between costFromCharacter χ on the mul of the two prime directions and the native onRatioOrbit of that same product. Downstream theorems discharge instances by introducing the primes and reducing to character rigidity or absolute-value identities.
why it matters
This field is the repaired third leg of admissible ratio characters after the two-adic countermodel: ratio-character laws, per-prime calibration, and prime-pair product cost consistency together keep the two global orientations while excluding valuation twists. It is required by PRCAdmissibleRatioCharacter and is the hypothesis that lets character_pair_two_calibration_forces_prime_calibration recover full prime-direction calibration from the pair field plus base two-calibration.
That transport feeds the slim and structural native-cost uniqueness ledgers (PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved, PRCStructuralNativeCostUniquenessTarget_proved), which close that the canonical cost is forced. In the broader Recognition chain this sits under J-uniqueness (T5) and the recognition composition law: native cost must be the unique admissible cost on the ratio lattice before continuum and physical constants are read off. Concrete characters (identity, absolute value) are shown to satisfy the field, anchoring the admissible class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.