absValueGeneratedNativeCost_prime_direction_cost

In the primitive recognition calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is the choice-free relation crossEq, which compares integer cross-multiples rather than forcing a classical rational quotient.

Native costs are maps $F$ on ratio orbits. The predicate PRCNativeCostPrimeDirectionCalibrated asserts all-prime calibration at the cost level: for every prime orbit $p$, $F$ on the prime direction of $p$ is cross-equal to the standard on-ratio-orbit of that direction. The module doc notes that Pass 283 refutes deriving this from two-point calibration alone, so the all-prime statement is a separate interface.

The map under study, absValueGeneratedNativeCost, is the native cost built from the absolute-value character: it sends the unit orbit to zero and otherwise applies costFromCharacter to absValueCharacter. Upstream, that character is already prime-calibrated, and the generated cost is cross-equal to the character cost on every orbit.

Term-mode after intro p hp. Apply RatioOrbit.crossEq_trans to chain two facts at the prime direction $q$ of $p$:

1. absValueGeneratedNativeCost_crossEq_generated q: the generated native cost is cross-equal to costFromCharacter absValueCharacter q.
2. absValueCharacter_prime_calibrated p hp: the abs-value character is prime-direction calibrated, so the character cost on $q$ is cross-equal to the standard on-ratio-orbit of $q`.

Transitivity of crossEq (choice-free, via the integer bridge) yields the cost-level calibration goal.

Closes the cost-level all-prime calibration interface for the absolute-value-generated native cost inside PRCNativeCostUniqueness. The defining predicate is explicitly the native-cost strengthening that cannot be recovered from two-point calibration alone (Pass 283), so this theorem is the direct discharge of that stronger demand for the abs-value generator.

It sits in the foundation layer that feeds Recognition Composition Law and J-uniqueness (T5): native costs are the discrete precursors of the continuous J-cost $J(x)=(x+x^{-1})/2-1$. Calibrating the generator on every prime direction locks the discrete cost against the prime-signed repaired interface before continuum limits or d'Alembert/trace matching are invoked.

No downstream consumers are recorded yet; the natural parents are uniqueness or matching theorems that assume PRCNativeCostPrimeDirectionCalibrated on a candidate native cost.