absValueGeneratedNativeCost_strengthened_hypotheses
plain-language theorem explainer
The absolute-value generated native cost on ratio orbits satisfies the strengthened native-cost interface: ordinary native axioms plus prime-pair product calibration. Cited when building the sans-sign class and when refuting uniqueness without a signed-unit probe. Proof is a structure wrapper that packages two already-proved component lemmas.
Claim. Let $F$ be the absolute-value generated native cost on ratio orbits. Then $F$ satisfies the strengthened native-cost hypotheses: it obeys the ordinary native-cost axioms (RCL, normalization, calibration) and is calibrated on products of distinct prime directions at the cost level.
background
In the Primitive Recognition Calculus, a native cost is a map $F$ on ratio orbits obeying the Recognition Composition Law together with normalization and calibration fields packaged as PRCNativeCostHypotheses. After the two-adic no-go, the interface is strengthened: keep those fields and add prime-pair product calibration at the cost level (PRCStrengthenedNativeCostHypotheses).
The absolute-value generated native cost sends the unit orbit to zero and otherwise applies the cost built from the absolute-value character. Upstream, it already satisfies the ordinary native hypotheses and the prime-pair product calibration predicate separately. This declaration only assembles those two facts into the strengthened structure.
proof idea
One-line structure wrapper. The native field is filled by absValueGeneratedNativeCost_native_hypotheses; the prime_pair_product_cost field is filled by absValueGeneratedNativeCost_prime_pair_product_cost. No new algebra is performed.
why it matters
Places the absolute-value cost inside the strengthened native interface used after the two-adic no-go. Downstream, absValueGeneratedNativeCost_sans_sign_hypotheses records that this cost inhabits the sans-sign class, and PRCAbsValueGeneratedCostStrengthenedNativeHypothesesTarget_constructed packages it as an explicit witness. The same fact feeds PRCStrengthenedNativeCostUniquenessTarget_refuted: uniqueness under strengthened hypotheses alone fails because this cost meets them yet mishandles the signed unit $-1$. That forces the signed-unit repair in the Recognition cost story (T5 J-uniqueness / RCL lineage), separating absolute-value probes from a fully canonical native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.