PRCNativeCostPrimePairProductCalibrated
plain-language theorem explainer
A native cost map F on ratio orbits is prime-pair product calibrated when, on every product of two native prime directions, F agrees with the canonical on-orbit cost display under cross-multiplication equality. Uniqueness and minimality deposits cite this as the cost-level patch that blocks the two-adic generated counterexample. The body is a pure Prop abbreviation, not a proved theorem.
Claim. A map $F$ from ratio orbits to ratio orbits is prime-pair product calibrated if, for every pair of prime distinction-orbits $p,r$, writing $u$ for the product of their prime directions, one has $\mathrm{crossEq}\bigl(F(u),\,C(u)\bigr)$, where $C$ is the canonical cost display on ratio orbits (the on-orbit $J$-cost).
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed orbit numerator over a nonzero distinction-orbit denominator. Two such displays are identified by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality).
Native costs are maps $F$ on these displays meant to realize the recognition cost. The older native-cost hypothesis pack already imposed reciprocity, normalization invariance, canonical RCL on nonzero orbits, unit-zero, and two-point calibration. That pack is insufficient: a two-adic axis twist still produces a generated cost that satisfies the old fields but fails uniqueness.
The repair is local. Prime directions are the orbit images of prime distinction-nats. This definition demands that $F$ already match the canonical on-orbit cost on every product of two such prime directions, exactly the surface where the two-adic counterexample slipped through.
proof idea
Definitional Prop, not a proved statement. The body quantifies over prime distinction-nats $p,r$ (with primality witnesses), forms the product of their prime directions, and asserts crossEq between $F$ of that product and the canonical onRatioOrbit cost of the same product. No tactics or lemmas are invoked at the definition site; downstream theorems discharge or package the field.
why it matters
This is the cost-level repair named in the strengthened native-cost interface after the two-adic no-go. Downstream, it appears as a required field in slim minimality certificates (PRCSlimSansRclHypotheses, PRCSlimSansTwoCalibrationHypotheses) and in the bridging iff that splits the zero-calibrated signed strengthened pack into a sans-pair base plus this pair calibration. The absolute-value generated native cost is proved to satisfy it, and the strengthened hypothesis structure packages it with the older RCL/normalization/calibration fields. In the Recognition forcing picture this protects uniqueness of the native cost toward the J-cost fixed by T5 and the RCL, by closing the exact loophole that let a non-canonical two-adic generator pass the pre-repair hypotheses. Premise ledgers for both the slim and full native cost-selection deposits list the necessity of this strengthening via the two-adic refutation of the older uniqueness target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.