PRCPrimeSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_of_character_factorization
plain-language theorem explainer
If every PRC-native RCL cost factors through a ratio character, then every cost that also carries prime-direction and signed-unit calibration factors through a signed-admissible character. Uniqueness arguments at the strengthened native-cost layer cite this upgrade. The proof lifts an ordinary factorization and transports prime and sign calibrations across cross-equality of ratio orbits.
Claim. Assume every map $F$ on ratio orbits that satisfies the native PRC cost hypotheses factors, up to cross-equality, as $F(q)=J(\chi(q))$ for some ratio character $\chi$. Then every $F$ that additionally satisfies the prime-signed strengthened native-cost hypotheses factors the same way through a signed-admissible ratio character (a character that is prime-direction calibrated, prime-pair product consistent, and signed-unit calibrated).
background
In the Primitive Recognition Calculus, costs live on ratio orbits: pairs of a signed numerator orbit and a nonzero distinction-nat denominator. Two orbits are identified by cross-equality when cross-multiplication of numerators and denominators balances as signed orbits (the internal PRC stand-in for rational equality).
The native J-cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$. A cost generated from a character $\chi$ is $J\circ\chi$. The native character-factorization target asserts that every admissible native RCL cost $F$ admits some ratio character $\chi$ with $F(q)$ cross-equal to $J(\chi(q))$ for all $q$: the discrete d'Alembert factorization step.
The strengthened target adds prime-direction calibration, prime-pair product cost consistency, and signed-unit calibration on $F$ itself. The conclusion asks for a signed-admissible character: ordinary character axioms plus those three calibrations on $\chi$.
proof idea
Fix $F$ with prime-signed strengthened native hypotheses. Apply the assumed native factorization to the underlying native hypotheses to obtain a ratio character $\chi$ with $F\simeq J\circ\chi$ pointwise under cross-equality.
Prime-direction calibration of $\chi$ is obtained by transporting $F$'s prime-direction cost along the factorization at each prime direction, using symmetry and transitivity of cross-equality. Prime-pair product consistency is the same transport at products of two prime directions.
Signed-unit calibration uses the factorization at the distinguished negative-one ratio together with $F$'s signed-unit hypothesis, then invokes the lemma that matching $J\circ\chi$ to native $J$ at negative one forces the character to be signed-unit calibrated. Package $\chi$ as signed-admissible and return the same pointwise factorization.
why it matters
This is the final repaired factorization bridge at the strengthened native-cost layer: ordinary character factorization plus cost-side prime and sign data already yield a signed-admissible factor, without a separate signed factorization axiom.
The sole downstream consumer is the uniqueness target theorem that reduces strengthened native-cost uniqueness to this signed-admissible factorization, then to uniqueness of signed-admissible characters. That sits inside the PRC native-cost uniqueness program, which aims to force the canonical J-cost (the T5 landmark $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$) as the unique RCL cost on ratio orbits.
Closing the native factorization hypothesis therefore upgrades automatically to the signed-admissible uniqueness pipeline used for the discrete recognition cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.