absValueGeneratedNativeCost_not_signed_unit_calibrated
plain-language theorem explainer
The absolute-value-generated native cost fails signed-unit calibration: it does not match the canonical cost at the orbit of −1. Anyone ruling out absolute-value characters as native costs cites this. The proof is a one-line wrapper of the already-proved failure of cross-equality at negativeOneRatio.
Claim. The native cost $F$ built from the absolute-value character is not signed-unit calibrated: $F$ applied to the ratio orbit of $-1$ is not cross-equal to the canonical on-orbit value at $-1$.
background
In the primitive recognition calculus, a native cost is a map $F$ on ratio orbits meant to realize the unique $J$-cost structure forced by the Recognition Composition Law. Signed-unit calibration is the repair condition after the absolute-value no-go: $F$ must see the signed unit $-1$, not only positive prime and prime-pair probes. Formally, $\mathrm{PRCNativeCostSignedUnitCalibrated}(F)$ asserts cross-equality of $F(-1)$ with the canonical on-orbit value at $-1$.
The absolute-value-generated native cost sends the unit orbit to zero and otherwise applies the cost built from the absolute-value character. Because absolute value collapses $-1$ with $+1$, that generator is the natural candidate to fail signed-unit calibration. The upstream lemma already shows the cross-equality at negativeOneRatio is false for this $F$.
proof idea
One-line wrapper: the claim is definitionally the negation of signed-unit calibration for this $F$, which is exactly the statement of absValueGeneratedNativeCost_negative_one_not_canonical. No extra algebra is needed.
why it matters
This pins the absolute-value generator as a concrete counterexample to signed-unit calibration, so it cannot serve as a repaired native cost. Downstream, it feeds the stronger no-go that the same $F$ fails the full signed strengthened native-cost hypotheses, and it refutes the target claiming zero-calibration alone forces signed-unit calibration. In the uniqueness program for the native cost (toward T5 $J$-uniqueness and the RCL), it closes the absolute-value loophole: any candidate that only probes positive data is eliminated once $-1$ is required.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.