reciprocal_character_prime_pair_product_cost_consistent
plain-language theorem explainer
The reciprocal map on ratio orbits is prime-pair product cost consistent: cost generated by reciprocity agrees with the native PRC cost on every product of two prime directions. Cited when packaging reciprocity as an admissible ratio character. Proof is a short term reduction through native reciprocal symmetry and symmetry of cross-equality.
Claim. The character $\chi(q)=q^{-1}$ on ratio orbits satisfies prime-pair product cost consistency: for all prime distinction naturals $p,r$, the cost generated by $\chi$ on the product of their prime directions is cross-equal to the native PRC cost of that same product.
background
Ratio orbits are rational displays: a signed-orbit numerator over a nonzero distinction-natural denominator. The native PRC cost on them is written onRatioOrbit. A character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ induces a cost by costFromCharacter $\chi,q=$ onRatioOrbit$(\chi q)$; the identity character recovers the native cost.
Prime-pair product cost consistency is the character-local demand that this induced cost agree with the native cost, under crossEq (balanced equality of signed orbits), on every product of two prime directions. It is one field of admissibility for a ratio character, distinct from the global calibration target that forces the same property from prime data alone.
Upstream, reciprocal symmetry of the native cost already gives crossEq(onRatioOrbit $q$, onRatioOrbit$(q^{-1})$) for every ratio orbit $q$, and crossEq is symmetric.
proof idea
Introduce primes $p,r$ and form the product $q$ of their prime directions. Apply reciprocal symmetry of the native cost to $q$, obtaining crossEq(onRatioOrbit $q$, onRatioOrbit$(q^{-1})$). Flip the two sides by symmetry of crossEq. Unfolding costFromCharacter then matches the goal exactly: costFromCharacter(recip,$q$) is onRatioOrbit$(q^{-1})$. The proof is a single simpa after those two lemmas.
why it matters
Discharges the prime_pair_product_cost field of PRCAdmissibleRatioCharacter for the reciprocal character, and is the sole cited ingredient for that field in reciprocal_admissible_ratio_character. Admissible characters are the candidates against which native-cost uniqueness is argued in the Primitive Recognition Calculus. Keeping reciprocity inside the admissible class embeds reciprocal symmetry of the cost (and ultimately of $J$, the T5 unique cost solving the Recognition Composition Law) into the character calculus rather than treating it as an external axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.