PRCSignedStrengthenedNativeCostUniquenessTarget_of_signed_admissible_factorization
plain-language theorem explainer
If every native signed-unit cost factors through a signed-admissible ratio character, then every such cost is cross-equal to the canonical native cost on every ratio orbit. Cited by the minimality refutation of signed factorization and by the two-calibration uniqueness bridge. Term proof: unpack the factor, then transit cross-equality through character rigidity.
Claim. Assume that every map $F$ on ratio orbits satisfying the signed-strengthened native cost hypotheses factors as $F(q)\sim\mathrm{cost}_\chi(q)$ for some signed-admissible ratio character $\chi$. Then every such $F$ satisfies $F(q)\sim\mathrm{onRatioOrbit}(q)$ for all ratio orbits $q$ (cross-equality of rational orbits).
background
In the Primitive Recognition Calculus, costs act on RatioOrbit displays: integer numerator over a nonzero distinction-nat denominator. Equality of displays is the choice-free relation crossEq, which identifies orbits that represent the same rational after clearing denominators.
The uniqueness target asks that any $F$ obeying the signed-strengthened native cost hypotheses (native cost field plus signed-unit calibration) agree with the canonical native cost onRatioOrbit at every orbit. The factorization hypothesis is weaker in form: it only demands some signed-admissible character $\chi$ with $F(q)$ cross-equal to the character-generated cost at every $q$.
Upstream, signed-admissible characters are already rigid: PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved shows that any such $\chi$ has character-cost cross-equal to onRatioOrbit. Transitivity of crossEq (via the integer bridge) therefore converts factorization into uniqueness.
proof idea
Term-mode proof. Fix $F$ and the strengthened hypotheses, then fix an orbit $q$. Apply the factorization hypothesis to obtain a signed-admissible character $\chi$ with $F(q)\sim\mathrm{costFromCharacter},\chi,q$. Feed $\chi$ into the proved rigidity theorem, which yields $\mathrm{costFromCharacter},\chi,q\sim\mathrm{onRatioOrbit},q$. Close by RatioOrbit.crossEq_trans.
why it matters
This is the signed-repair bridge (post pass 281) from character factorization to native-cost uniqueness under signed-unit calibration. Downstream, PRCSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted uses it contrappositively: uniqueness is already refuted for the zero-flat cost, so signed-admissible factorization cannot hold for every inhabitant. The sibling bridge ..._of_character_factorization_and_two_calibration routes ordinary character factorization plus two-calibration through this lemma to reach the same uniqueness target.
In the Recognition forcing picture this sits under native $J$-cost uniqueness (T5 lineage): admissible characters are forced onto the canonical cost, so factorization would pin every calibrated native cost to onRatioOrbit. The refutation path shows that full signed factorization is too strong, sharpening which calibration hypotheses can survive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.