PRCStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget
plain-language theorem explainer
Defines the repaired factorization target for strengthened native costs: every cost map obeying the strengthened hypotheses must factor, up to cross-equivalence of ratio orbits, through some signed-admissible rational character. Cited by the uniqueness-from-factorization bridge and by the theorem that refutes the target. Pure Prop packaging; no proof content.
Claim. For every map $F$ on ratio orbits that satisfies the strengthened native-cost hypotheses (ordinary native-cost axioms plus prime-pair product calibration), there exists a signed-admissible ratio character $\chi$ such that for every ratio orbit $q$, $F(q)$ is cross-equivalent to the cost generated from $\chi$ at $q$.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is internal cross-multiplication (crossEq): two orbits match when the scaled numerators balance as signed orbits.
A cost generated from a character $\chi$ is the orbit map $q \mapsto$ the on-ratio-orbit image of $\chi(q)$; the identity character recovers the canonical PRC cost. The signed-admissible character interface strengthens ordinary admissibility by requiring explicit preservation of the signed unit (the unsigned interface alone was already shown not to force this).
After the two-adic no-go, native-cost hypotheses were strengthened: keep RCL, normalization, and calibration, and add prime-pair product calibration at the cost level. This definition packages the claim that every such strengthened cost factors through a signed-admissible character.
proof idea
Definitional Prop only: the body is the universal-existential statement above, assembled from the named hypothesis structures and the cross-equivalence relation. No tactics, no lemmas applied. Downstream proofs treat the name as a black-box hypothesis or as the proposition to negate.
why it matters
This is the repaired factorization target in the native-cost uniqueness thread: strengthened costs must factor through signed-admissible characters, not merely the unsigned admissible interface already refuted via absolute-value characters.
It feeds two local results. First, assuming the target yields the strengthened uniqueness target: if $F$ factors through some signed-admissible $\chi$, cross-equivalence of $F(q)$ with the character cost, plus transitivity of cross-equivalence, pins $F$ to the unique native cost. Second, the target itself is refuted by reducing uniqueness-from-factorization to the already-refuted uniqueness target.
In the broader Recognition chain this sits under native $J$-cost uniqueness (T5 / RCL territory): it records that even the signed repair of the character interface cannot salvage a factorization route to uniqueness for strengthened native costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.