PRCNativeCostPrimeDirectionCalibrated
plain-language theorem explainer
Native cost-level all-prime calibration: a map F on ratio orbits agrees, under cross-multiplication, with the native J-cost display on every prime direction. Downstream uniqueness, minimality, and the prime-signed strengthened native-cost interface cite it as a hypothesis field. Pure Prop definition: a universal quantifier over prime distinction orbits, not a derived theorem.
Claim. A map $F$ from ratio orbits to ratio orbits is prime-direction calibrated when, for every prime distinction orbit $p$, $F$ applied to the prime direction of $p$ is cross-multiplication equivalent to the native cost display of that same prime direction.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed numerator orbit over a nonzero distinction-orbit denominator. Two such displays are related by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality).
DistinctionNat is the base-neutral finite orbit of repeated distinction; primeOrbit marks the primes in that hierarchy, and primeDirection sends each such prime to its corresponding ratio-orbit axis. The native cost display onRatioOrbit is the J-cost (Recognition Composition Law cost, $J(x)=(x+x^{-1})/2-1$) evaluated on that axis.
The surrounding module builds native-cost uniqueness and selection interfaces. Cost appears upstream as total recognition cost under a ratio weight, as the cost induced by a multiplicative recognizer, and as the J-cost of a recognition event. This definition isolates the all-prime calibration demand at the cost level itself.
proof idea
Definition only: the body is the proposition that for every prime distinction orbit $p$ (with primeOrbit witness), crossEq holds between $F$ of the prime direction and the native onRatioOrbit display of that direction. No tactics, no lemmas applied; it packages a universal calibration constraint for later hypothesis structures and theorems.
why it matters
This is the cost-level all-prime calibration atom in the native-cost uniqueness stack. The doc-comment records that Pass 283 refutes deriving it from two-calibration alone, so it must be stated (or recovered from a stronger package) rather than omitted.
It is a field of PRCPrimeSignedStrengthenedNativeCostHypotheses (signed strengthened hypotheses plus this calibration). Downstream, all_prime_axis_field_redundant shows every inhabitant of the slim zero-calibrated signed-strengthened ledger automatically satisfies it; absValueGeneratedNativeCost_prime_direction_cost checks the absolute-value generated native cost meets it; and nativeCostSelectionPremiseLedger itemizes related selection premises.
Framework link: calibration of the native cost on prime axes is the discrete counterpart of forcing the unique J-cost (T5 / RCL) along the multiplicative generators of the ratio lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.