PRCNoSignedAdmissibleFactorForAbsValueGeneratedNativeCost
plain-language theorem explainer
No signed admissible ratio character can reproduce the absolute-value-generated native cost on every ratio orbit (under cross-equivalence). Cost-uniqueness and character-factorization arguments in PRC cite this obstruction. The proof evaluates at the negative-one orbit, transports via signed-character rigidity to the canonical J-cost, and contradicts the known non-canonicity of the abs-value cost at −1.
Claim. There is no map $\chi$ from ratio orbits to ratio orbits that is a signed admissible ratio character (prime/prime-pair admissibility plus signed-unit calibration) and satisfies, for every ratio orbit $q$, $$\mathrm{crossEq}\bigl(C_{|\cdot|}(q),\, C_\chi(q)\bigr),$$ where $C_{|\cdot|}$ is the absolute-value-generated native cost and $C_\chi$ is the cost built from $\chi$.
background
In the Primitive Recognition Calculus, costs and characters live on RatioOrbit objects: integer numerator over a nonzero distinction-nat denominator. Equality of displays is the internal relation crossEq, cross-multiplication balance of scaled signed orbits (K4.10), not bare rational equality of verifier displays.
The canonical rational J-cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$, written onRatioOrbit. A native cost may instead be generated from a ratio character via costFromCharacter. The absolute-value-generated native cost is the special case that uses the absolute-value character away from the unit orbit (and zero at one).
Signed admissibility strengthens ordinary admissible characters by requiring explicit preservation of the signed unit. The module develops uniqueness and factorization targets for zero-calibrated native costs against such signed characters; the present theorem is a concrete negative instance for the abs-value generator.
proof idea
Term-mode proof by contradiction. Unpack a putative signed admissible $\chi$ and the pointwise crossEq factorization hypothesis. Specialize at negativeOneRatio. Transitivity of crossEq composes the factorization identity with the signed-admissible rigidity lemma (PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved), which forces the character-cost at $-1$ to match the canonical onRatioOrbit value. The composite therefore asserts crossEq between absValueGeneratedNativeCost(-1) and onRatioOrbit(-1). That is exactly what absValueGeneratedNativeCost_negative_one_not_canonical denies, yielding the contradiction.
why it matters
This is the local obstruction that discharges the signed-admissible factorization target for the abs-value native cost. The sole downstream consumer is PRCZeroCalibratedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted, which applies the theorem at absValueGeneratedNativeCost under its native hypotheses and thereby refutes the zero-calibrated signed factorization claim.
In the broader Recognition stack this sits inside native-cost uniqueness for PRC, upstream of the forcing-chain identification of $J$ (T5: $J(x)=(x+x^{-1})/2-1$). It shows that absolute-value generation, while a natural candidate character cost, is incompatible with signed unit calibration at the negative unit, so any uniqueness route that demands signed-admissible factorization must exclude or repair that generator. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.