absValueCharacter_two_cost_calibrated
plain-language theorem explainer
The absolute-value character is cost-calibrated at the ratio orbit 2: the cost rebuilt from that character agrees with the native PRC J-cost on 2 under cross-multiplication equality of ratio orbits. Anyone tracking character-to-cost rigidity cites this as the positive calibration half of the counterexample. The proof specializes the prime-orbit calibration lemma at the two-orbit and rewrites via the two-prime-direction identification.
Claim. Let $\chi_{|\cdot|}$ be the absolute-value character on ratio orbits and let $C_\chi$ be the cost reconstructed from a character. Then $C_{\chi_{|\cdot|}}(2)$ and the native $J$-cost $J(2)=((2+2^{-1})/2)-1$ are equivalent as ratio orbits under cross-multiplication (balanced scaled numerators and denominators).
background
In the Primitive Recognition Calculus, rationals are displayed as RatioOrbit objects: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of such displays is internal: crossEq holds when the cross-multiplied signed orbits balance (K4.10), so no external real field is required.
The native cost on a ratio orbit is the PRC J-object $J(q)=((q+q^{-1})/2)-1$, built by orbit arithmetic (onRatioOrbit). Separately, an absolute-value character $\chi_{|\cdot|}$ sends each ratio orbit to the orbit display of $|q|$ as a real; it respects the ratio character axioms but erases the sign of $-1$. From any such character one rebuilds a candidate cost via costFromCharacter.
This lemma sits in the native-cost uniqueness module: it checks whether that rebuilt cost matches native $J$ at the distinguished point $2$ (the two-step orbit over unit denominator).
proof idea
One-line specialization. Invoke absValueCharacter_prime_calibrated at twoOrbit, using that the two-orbit is a prime orbit (twoOrbit_primeOrbit). The resulting calibration identity is then rewritten by simpa along the definitions twoPrimeDirection and primeDirection, which identify the two-orbit direction with the generic prime-direction packaging used by the prime-calibration statement. No new arithmetic is performed.
why it matters
This is the positive half of the rigidity counterexample. Downstream, PRCNativeCostCharacterRigidityTarget_refuted assumes a rigidity target that demands every ratio character calibrated at $2$ to reproduce native cost everywhere, then feeds in absValueCharacter together with this calibration and the ratio-character certificate; the target collapses because the same character fails to be canonical at $-1 (absValueCharacter_negative_one_cost_not_canonical`).
In framework terms the native $J$ is the T5 cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). Showing that absolute-value matching at $2$ does not force full character rigidity protects the uniqueness story: calibration at a single positive generator is too weak, so the forcing chain must retain the full d'Alembert / composition-law package rather than a thin character axiom at $2$ alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.