PRCCharacterPrimeDirectionCalibrated
plain-language theorem explainer
A ratio character χ is prime-direction calibrated when the cost it induces agrees with the canonical J-cost, under cross-multiplication equality of ratio orbits, on every native prime orbit. Downstream uniqueness and admissibility results cite this as the per-prime calibration field. The body is a universal Prop over prime distinction-orbits, not a proved theorem.
Claim. A map $\chi$ on ratio orbits is prime-direction calibrated if, for every prime distinction-orbit $p$, the cost generated by $\chi$ on the prime direction of $p$ is cross-multiplication equivalent to the canonical $J$-cost display of that same prime direction.
background
In the Primitive Recognition Calculus, rational data live as ratio orbits: a signed-orbit numerator over a nonzero distinction-natural denominator. Two ratio orbits are identified by cross-multiplication equality (crossEq): the scaled numerators balance as signed orbits, the internal PRC stand-in for rational equality without leaving the orbit language.
A ratio character $\chi$ is a map on ratio orbits. From it one builds an induced cost on orbits (costFromCharacter). The canonical comparison cost is the native $J$-display on the same orbit (onRatioOrbit). Prime directions are the ratio-orbit axes attached to prime distinction-naturals.
This module packages native-cost uniqueness targets. The present definition isolates the per-prime calibration condition that later uniqueness and admissibility interfaces require: induced cost must match canonical $J$ on every prime axis, not merely at a base two-point ledger.
proof idea
Definitional Prop, not a proof. Unfolding yields a double universal quantifier over prime distinction-naturals $p$ (with a primality witness) asserting cross-multiplication equality between costFromCharacter χ and the canonical onRatioOrbit display, both evaluated at the prime direction of $p$. No tactics or lemmas fire at the definition site; downstream theorems discharge or assume the Prop.
why it matters
This is the repaired per-prime calibration field after the two-adic countermodel. It appears inside the admissible-character interface (PRCAdmissibleRatioCharacter), which demands ratio-character laws, prime calibration, and prime-pair product cost consistency so that global orientations survive while valuation twists are excluded.
Minimality work uses it as the conclusion of the transport lemma that two-point calibration at orbit 2, plus prime-pair product consistency, forces calibration on every native prime axis, closing a gap where independent prime axes previously lacked control. Absolute-value and identity characters are shown to satisfy it. Zero-calibrated and structural native-cost uniqueness targets route through this field when recovering $J$ from ledger hypotheses.
In the broader RS forcing picture this is local bookkeeping toward T5 $J$-uniqueness: native cost must lock to $J(x)=(x+x^{-1})/2-1$ on the prime generators before global uniqueness can close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.