PRCZeroCalibratedPrimeSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_proved
plain-language theorem explainer
Under zero-calibrated, prime-signed, strengthened native-cost hypotheses, a cost map on ratio orbits factors as the native J-cost of a signed-admissible character. Native J-cost uniqueness proofs in the Primitive Recognition Calculus cite this factorization. The argument lifts the unsigned zero-calibrated factorization and repairs prime-direction, pair-product, and signed-unit calibration by transporting cross-equivalence.
Claim. Let $F$ be a map on ratio orbits satisfying the zero-calibrated prime-signed strengthened native-cost hypotheses. Then there exists a signed-admissible ratio character $\chi$ such that for every ratio orbit $q$, $F(q)$ is cross-equivalent to the native $J$-cost evaluated at $\chi(q)$: $F(q)\sim J(\chi(q))$ under the internal cross-multiplication relation on ratio orbits.
background
Primitive Recognition Calculus works with ratio orbits: integer numerator over a nonzero distinction-nat denominator, the internal rational display. Two orbits are related by cross-equivalence when scaled numerators balance as signed orbits (the choice-free stand-in for rational equality).
The native cost on a ratio orbit is the PRC $J$-object $J(q)=((q+q^{-1})/2)-1$. Cost generated from a character $\chi$ is simply $J\circ\chi$. A signed-admissible ratio character is a character that is prime-direction calibrated, prime-pair product consistent, and signed-unit calibrated at the negative-one orbit.
The local setting is zero-calibrated native-cost uniqueness: the repaired hypothesis package is meant to be strong enough that the zero-calibrated trace-root factor becomes a signed-admissible character, so $F$ matches cost-from-character everywhere.
proof idea
Apply the already-proved zero-calibrated (unsigned) character factorization to the native fragment of the hypotheses, obtaining $\chi$ with $F\sim J\circ\chi$ pointwise under cross-equivalence.
Prime-direction calibration of $\chi$ is recovered by transporting the cost's prime-direction data across the factorization via symmetry and transitivity of cross-equivalence. Prime-pair product consistency is the same transport on products of prime directions.
Signed-unit calibration: the factorization at the negative-one orbit, composed with the hypothesis that $F$ matches native $J$ there, yields $J(\chi(-1))\sim J(-1)$; the lemma that cost-from-character at negative one forces the signed unit then upgrades $\chi$ to signed-unit calibrated. Package the three calibration pieces into signed admissibility and return the same pointwise factorization.
why it matters
This is the repaired final factorization step for zero-calibrated native cost: hypotheses strong enough to promote the trace-root factor to a signed-admissible character. The immediate parent is the uniqueness target that, given this factorization, concludes $F$ agrees with native $J$ on every orbit.
In the broader Recognition chain this sits under T5 $J$-uniqueness: the cost forced by the Recognition Composition Law is $J(x)=(x+x^{-1})/2-1$. Here the same identity is recovered internally on ratio orbits from a character factorization, without leaving the PRC display language.
It also feeds the native-cost uniqueness blocker certificate machinery in the module, marking which strengthened hypothesis packages close versus which remain refuted. The open question it closes is whether zero calibration plus prime-signed strengthening already yields signed admissibility; this theorem answers yes for the factorization target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.