PRCAbsValueGeneratedCostStrengthenedNativeHypothesesTarget
plain-language theorem explainer
Packages the exact no-go target after signed-unit analysis: some cost map on rational ratio orbits obeys the strengthened native-cost interface (RCL, normalization, calibration, plus prime-pair product calibration) and agrees, under cross-multiplication, with the cost generated by the absolute-value character. That character erases the sign of −1. Uniqueness and no-go arguments cite this Prop as the precise counterexample shape. The body is a pure existential definition, not a proof.
Claim. There exists a map $F$ from ratio orbits to ratio orbits such that $F$ satisfies the strengthened native-cost hypotheses (the ordinary native-cost package together with prime-pair product calibration at the cost level), and for every ratio orbit $q$, $F(q)$ is cross-multiplication equivalent to the cost generated from the absolute-value character on $q$.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are identified by cross-multiplication when the scaled numerators balance as signed orbits; that internal relation is the PRC stand-in for rational equality.
A rational character is a map on ratio orbits. The absolute-value character sends each display to the ratio-orbit of the absolute value of its verifier rational, so it is a quotient-respecting character that erases the sign of $-1$. Cost generated from a character is the character composed with the on-ratio-orbit cost construction; the identity character recovers the canonical PRC cost.
After the two-adic no-go, the strengthened native-cost interface keeps the old RCL, normalization, and calibration fields and adds prime-pair product calibration at the cost level. This module sits in the native-cost uniqueness development that isolates which characters can still produce a native cost once that repair is imposed.
proof idea
Definitional packaging only: the Prop is the existential assertion that some $F : \mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ satisfies the strengthened native-cost structure and is pointwise cross-equivalent to cost-from-character of the absolute-value character. No tactics or lemmas are invoked at this declaration; witnesses are supplied by the downstream construction theorem.
why it matters
Pins the exact strengthened-hypothesis no-go target after signed-unit analysis: absolute value still generates a native cost that passes the prime-pair repair while deleting signed units. The downstream theorem PRCAbsValueGeneratedCostStrengthenedNativeHypothesesTarget_constructed discharges the Prop by exhibiting the absolute-value-generated native cost and verifying the strengthened hypotheses plus pointwise cross-equivalence.
In the broader Recognition chain this constrains cost uniqueness (T5 J-uniqueness and the Recognition Composition Law). Any claim that native cost is forced to the canonical J-cost must rule out, or carefully quotient by, absolute-value collapse of the signed unit. The target therefore separates genuine uniqueness from uniqueness only up to sign erasure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.