absValueGeneratedNativeCost_not_signed_strengthened_hypotheses
plain-language theorem explainer
The absolute-value generated native cost fails the signed strengthened native-cost interface. Anyone ruling out absolute-value candidates after the absolute-value no-go cites this. The proof is a one-line projection: the signed-unit calibration conjunct already fails, so the full hypothesis bundle cannot hold.
Claim. Let $F_{|\cdot|}$ be the native cost generated from the absolute-value character on ratio orbits (sending the unit orbit to zero and otherwise applying the character cost). Then $F_{|\cdot|}$ does not satisfy the signed strengthened native-cost hypotheses: it fails the package consisting of the strengthened native-cost axioms together with direct calibration at the signed unit.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits meant to realize the unique J-cost of the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). After an absolute-value no-go, uniqueness is restated only for costs that also calibrate the signed unit.
PRCSignedStrengthenedNativeCostHypotheses packages that repaired interface: the pass-274 strengthened native-cost hypotheses plus PRCNativeCostSignedUnitCalibrated. The absolute-value generated native cost is the candidate built from the absolute-value character: it sends the unit orbit to zero and otherwise applies costFromCharacter of that character.
An upstream theorem already shows this candidate is not signed-unit calibrated (via failure at the negative unit / non-canonical value). The present result lifts that failure to the full signed strengthened bundle.
proof idea
One-line wrapper. Assume the signed strengthened hypotheses hold for the absolute-value generated native cost. Project to the signed_unit field and discharge by the upstream theorem that this cost is not signed-unit calibrated (absValueGeneratedNativeCost_not_signed_unit_calibrated, itself a thin wrapper of the negative-one non-canonicality fact).
why it matters
Closes a no-go branch in native-cost uniqueness: absolute-value generation cannot meet the post-pass-281 uniqueness target, which asks uniqueness only among costs that calibrate the signed unit. That target is the repaired interface after the absolute-value no-go (doc: "uniqueness is now asked only for native costs that also calibrate the signed unit").
Framework link is T5 J-uniqueness and the Recognition Composition Law: only the genuine J-cost (not an absolute-value surrogate) is allowed to sit as the native cost. No downstream consumers are wired yet; the lemma is a local exclusion step inside PRCNativeCostUniqueness, clearing the absolute-value candidate so uniqueness arguments need not entertain it under the strengthened signed hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.