PRCZeroCalibrationForcesNativeCostSignedUnitCalibrationTarget_refuted
plain-language theorem explainer
Zero-calibration of the doubled trace does not force signed-unit calibration on native cost maps. The absolute-value character cost is a concrete counterexample: it meets the native-cost hypotheses and has zero-calibrated doubled trace, yet fails signed-unit calibration. Anyone tracking uniqueness blockers for the PRC native cost cites this. The proof is a one-shot counterexample application.
Claim. It is not the case that every map $F$ on ratio orbits satisfying the native-cost hypotheses and whose doubled-trace cost is zero-calibrated must be signed-unit calibrated. Equivalently, zero-calibration of the doubled trace does not force signed-unit calibration for native costs.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits obeying reciprocity and related structural hypotheses (PRCNativeCostHypotheses). From $F$ one builds a doubled-trace functional; zero-calibration of that doubled trace means the doubled-trace value vanishes at the unit orbit in the expected way.
Signed-unit calibration is a stronger normalization: it requires the cost to treat signed units (in particular the orbit of $-1$) in a canonical way. The absolute-value-generated native cost is built from the absolute-value character: it sends the unit orbit to zero and otherwise applies the cost-from-character construction for the absolute-value character.
Upstream facts already establish that this absolute-value cost satisfies the native-cost hypotheses, that its doubled trace is zero-calibrated, and that it is nevertheless not signed-unit calibrated (it fails on the negative-one orbit).
proof idea
Assume for contradiction the universal implication: every native-cost $F$ with zero-calibrated doubled trace is signed-unit calibrated. Instantiate that implication at the absolute-value-generated native cost, feeding the already-proved native hypotheses and the already-proved zero-calibration of its doubled trace. The conclusion would be signed-unit calibration of that cost, which directly contradicts the upstream lemma that the absolute-value-generated cost is not signed-unit calibrated. Discharge by that contradiction.
why it matters
Native-cost uniqueness is a foundation gate in PRC: if zero-calibration alone forced signed-unit calibration, the uniqueness story would close more tightly. This refutation shows that gate fails, so uniqueness needs a stronger package of hypotheses.
It is consumed by the native-cost uniqueness blocker certificate, which records which factorization and calibration targets are proved versus refuted. That blocker in turn feeds the conditional universal-foundation certificate in UniversalFoundation, keeping the foundation stack honest about what zero-calibration does and does not buy.
In the broader Recognition forcing chain this sits upstream of J-uniqueness and the RCL: cost calibration must be pinned before the self-similar fixed point and eight-tick structure can be forced cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.