identity_character_prime_pair_product_cost_consistent
plain-language theorem explainer
The identity map on rational orbits satisfies prime-pair product cost consistency: on every product of two native prime directions, character-generated cost matches the canonical ratio-orbit cost. Anyone assembling an admissible ratio character cites this field. The proof is a one-line specialization of identity rigidity to that product orbit.
Claim. The identity character $\chi(q)=q$ on rational orbits is prime-pair product cost consistent: for every pair of native prime orbits $p,r$, writing $d_p,d_r$ for their prime directions, the cost generated by $\chi$ on $d_p\cdot d_r$ is cross-equal to the canonical cost on that same product orbit.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters are maps $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$; each induces a cost via costFromCharacter, compared to the canonical cost onRatioOrbit by the cross-equality relation on orbits.
Prime directions package native prime orbits as ratio orbits. Prime-pair product cost consistency asks that, for every pair of primes, character cost and canonical cost agree on the product of those directions. The character-local form is a field of admissibility, not a global forcing target.
Upstream, identity rigidity already asserts that for every rational orbit $q$, cost from the identity character on $q$ is cross-equal to the canonical cost on $q$. The present statement only needs that fact on products of prime directions.
proof idea
Term-mode specialization. Introduce primes $p,r$ with their prime-orbit witnesses, form the product orbit of the two prime directions, and apply identity rigidity at that single orbit. No extra algebra: the universal quantifier in rigidity covers the product case.
why it matters
Feeds directly into identity_admissible_ratio_character, which packages the identity map as a full admissible ratio character (ratio-character axioms, prime calibration, and this prime-pair product field). Admissibility is the gate for native-cost uniqueness arguments in PRC: only admissible characters are candidates for the unique cost that matches the J-cost structure forced later in the chain (T5 J-uniqueness and the Recognition Composition Law). Without this field filled for the identity, the identity could not sit in the admissible class used to pin native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.