PRCAbsValueGeneratedCostStrengthenedNativeHypothesesTarget_constructed
plain-language theorem explainer
Existence of a native cost map on ratio orbits generated by the absolute-value character that meets the strengthened native-cost hypotheses (including the prime-pair repair) and agrees, via cross-equality, with the absolute-value character cost at every orbit. Anyone tracking the signed-unit no-go in primitive recognition calculus would cite it. The proof is a three-field existential package of prior constructions.
Claim. There exists a map $F$ from ratio orbits to ratio orbits such that $F$ satisfies the strengthened native-cost hypotheses, and for every ratio orbit $q$, $F(q)$ is cross-equal to the cost induced by the absolute-value character at $q$.
background
In the primitive recognition calculus, costs on ratio orbits can be induced from multiplicative characters via a standard conversion. The absolute-value character is the unsigned magnitude character; it deliberately erases signed-unit data that finer characters retain.
The strengthened native-cost package asks for the usual native axioms plus a prime-pair product repair. Cross-equality is the native identification relation on ratio-orbit values used throughout this module when comparing two cost presentations.
The target proposition is the exact strengthened-hypothesis no-go after the signed-unit analysis: it asserts that some native cost $F$ both satisfies those strengthened hypotheses and matches the absolute-value character cost on every orbit. Upstream, that $F$ is built by sending the unit orbit to zero and otherwise applying the absolute-value character cost, with separate lemmas verifying the strengthened package and the cross-equality identity.
proof idea
Term-mode existential introduction. The witness map is the absolute-value-generated native cost (unit orbit to zero; otherwise the absolute-value character cost). The two conjuncts are supplied by the already-proved lemmas that this map satisfies the strengthened native-cost hypotheses and that it is cross-equal, orbitwise, to the absolute-value character cost. No further rewriting is required.
why it matters
Closes the constructive half of the strengthened-hypothesis no-go after signed-unit analysis: the absolute-value character really does generate a native cost that passes the prime-pair repair while discarding signed-unit structure. That fact is the obstruction side of native-cost uniqueness arguments in the primitive recognition calculus, which sit upstream of the J-cost uniqueness landmark (T5) and the Recognition Composition Law. No downstream consumers are wired yet; the declaration stands as the packaged existence target those uniqueness or classification proofs will invoke.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.