PRCAdmissibleCharacterSignedUnitCalibratedTarget_refuted
plain-language theorem explainer
Every admissible ratio character need not be signed-unit calibrated: the absolute-value character is admissible yet sends the orbit of $-1$ to $+1$. Native-cost uniqueness and foundation-certificate work cite this as a blocker on the current admissibility interface. The proof is a direct counterexample instantiation of the universal claim.
Claim. It is false that every admissible ratio character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ is signed-unit calibrated. Equivalently, there exists an admissible ratio character that fails signed-unit calibration (in particular, the absolute-value character on rational displays).
background
In the Primitive Recognition Calculus, ratio characters are maps on ratio orbits (quotient displays of positive/negative rationals used by the verifier). Admissibility packages three fields: being a genuine ratio character, prime calibration, and a prime-pair product-cost law. Signed-unit calibration is a stronger demand: the character must preserve the orbit of $-1$ rather than collapse sign.
The absolute-value character sends each orbit to the orbit of $|q|$. Upstream, it is proved admissible (ratio character, prime-calibrated, prime-pair product cost) and separately proved not signed-unit calibrated: evaluating on the negative-one orbit yields a numerical contradiction after reducing through toRat.
The target proposition asserts that admissibility alone already forces signed-unit calibration for every character. The module records (Pass 279) that the repaired prime-pair admissibility fields still fail to enforce that constraint.
proof idea
Term-mode reductio. Assume the target (every admissible character is signed-unit calibrated). Instantiate at the absolute-value character and feed its admissibility theorem to obtain signed-unit calibration of that character. Discharge by the upstream lemma that the absolute-value character is not signed-unit calibrated (it equates the image of $-1$ with $+1$ after toRat reduction and norm_num).
why it matters
This is a negative interface result, not a uniqueness theorem. It certifies that the present admissible-character package does not pin down signed units, so native cost cannot yet be forced unique from admissibility alone. Downstream it feeds prc_native_cost_uniqueness_blocker_certificate, which aggregates such gaps into the native-cost uniqueness blocker, and appears in the dependency cone of prc_universal_foundation_conditional_certificate.
In the broader Recognition forcing picture, cost uniqueness ultimately targets the J-cost $J(x)=(x+x^{-1})/2-1$ (T5) via the Recognition Composition Law. Signed-unit calibration is a necessary side condition so that characters do not erase orientation before the doubled-trace/d'Alembert route reconstructs $J$. Closing the gap means strengthening admissibility until this refutation no longer applies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.