absValueCharacter_prime_calibrated
plain-language theorem explainer
The absolute-value ratio character is calibrated on every native prime direction: the cost it generates on each prime orbit agrees with canonical J-cost. Cited when assembling admissibility of that character or when checking native-cost hypotheses for the cost it generates. Proof is a short congruence: the character fixes prime directions, so the orbit J-cost map preserves the equality.
Claim. The absolute-value character $\chi_{\mathrm{abs}}$ on ratio orbits is prime-direction calibrated: for every native prime $p$ with prime-orbit witness $h_p$, the cost generated by $\chi_{\mathrm{abs}}$ on the prime direction of $p$ is cross-equal to the canonical $J$-cost on that same prime direction.
background
In the Primitive Recognition Calculus, ratio orbits quotient rational verifier displays under recognition equivalence. A ratio character $\chi$ is a self-map of ratio orbits used to generate a candidate native cost via costFromCharacter. The absolute-value character sends each orbit to the orbit of the absolute value of its rational representative; it respects the ratio structure but erases the sign of $-1$.
Prime directions are the orbits attached to native primes (DistinctionNat primes). A character is prime-direction calibrated when, on every such orbit, the generated cost agrees with the canonical embedding of $J$-cost on ratio orbits (cross-equality). That universal statement is exactly PRCCharacterPrimeDirectionCalibrated.
Upstream, the prime-identity lemma already shows $\chi_{\mathrm{abs}}$ fixes every prime direction up to cross-equality. The congruence lemma for the orbit $J$-cost map lifts any such cross-equality through that map.
proof idea
Short term proof. Introduce the native prime $p$ and its prime-orbit witness. Apply the orbit-$J$-cost congruence lemma to the absolute-value prime-identity at $(p,h_p)$. That identity gives cross-equality between $\chi_{\mathrm{abs}}$ on the prime direction and the prime direction itself; congruence pushes the equality through the canonical orbit $J$-cost map, which is the calibration goal for this character.
why it matters
Supplies the prime-calibration conjunct of admissibility for the absolute-value character, and is specialized immediately to two-cost calibration at the orbit of $2$. Downstream it also feeds the native-cost hypothesis package and the prime-direction cost calibration for the native cost generated by that character.
On the Recognition side this is discrete/rational-display work toward native-cost uniqueness, the PRC counterpart of $J$-uniqueness (T5) and the Recognition Composition Law. Calibrating $\chi_{\mathrm{abs}}$ on every prime axis is required before claiming the generated cost matches canonical $J$ on the prime skeleton. The module's sharper target A (two-point calibration at orbit $2$ forcing all prime axes) remains a separate control problem; this lemma is the direct prime-by-prime verification for absolute value, not that forcing argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.