PRCSignedStrengthenedNativeCostUniquenessTarget_of_character_factorization_and_two_calibration
plain-language theorem explainer
Character factorization of admissible PRC-native RCL costs, plus the claim that two-point calibration at orbit 2 forces prime-direction calibration, jointly imply uniqueness for signed-strengthened native costs. Cite this when closing the native-cost uniqueness chain at the signed-unit layer. The proof is a pure term composition through the signed-admissible factorization intermediate.
Claim. Assume every admissible PRC-native RCL cost $F$ factors through some ratio character $\chi$ (so $F(q)$ is cross-equal to the character cost of $\chi$ at every ratio orbit $q$), and assume that calibration of a character cost at orbit $2$ forces calibration on every prime direction. Then every signed-strengthened native cost $F$ satisfies $F(q)\simeq q$ (cross-equality with the canonical orbit cost) for all ratio orbits $q$.
background
In the Primitive Recognition Calculus (PRC), costs live on ratio orbits and are constrained by the Recognition Composition Law (RCL), the discrete form of the d'Alembert identity behind the J-cost $J(x)=(x+x^{-1})/2-1$. An admissible PRC-native cost is one obeying the native cost hypotheses (RCL-type identities and calibration data on the orbit monoid).
The first exact blocker is character factorization: every such $F$ should arise as $\mathrm{costFromCharacter},\chi$ for a ratio character $\chi$ (a multiplicative map on ratio orbits). Separately, two-point calibration at the orbit of $2$ is asked to force calibration along every prime direction; that is the prime-axis rigidity step. Signed-strengthened uniqueness then asks only for native costs that also calibrate the signed unit: such an $F$ must be cross-equal to the canonical orbit cost $\mathrm{onRatioOrbit}$ at every $q$.
This module packages those targets as Props and chains the reductions that turn factorization-plus-calibration into uniqueness.
proof idea
Pure term-mode composition, no tactics. First apply the intermediate
PRCSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_of_character_factorization_and_two_calibration
to the two hypotheses (ordinary character factorization, and two-calibration forces prime calibration). That yields signed-admissible character factorization: ordinary factorization plus the two-calibration hypothesis produce a factor that is admissible at the signed-unit layer.
Then feed that result into
PRCSignedStrengthenedNativeCostUniquenessTarget_of_signed_admissible_factorization,
which is the one-step implication from signed-admissible factorization to the signed-strengthened uniqueness target. The whole proof is therefore a two-lemma wrapper.
why it matters
This is a glue theorem in the native-cost uniqueness stack for PRC. It reduces the signed-strengthened uniqueness target to two named surface targets: discrete d'Alembert character factorization, and the two-to-prime calibration forcing step. In the broader Recognition Science forcing chain this sits under T5 J-uniqueness: once native costs are forced to the canonical orbit cost (the discrete avatar of $J$), the continuous J-cost and the RCL identity are the only remaining analytic lift.
No downstream consumers are wired yet (used_by_count = 0), so the declaration is presently a leaf in the dependency graph: it records that the repaired signed-unit uniqueness target is discharged once the two upstream blockers are closed. The open work is therefore not here but in proving those two hypothesis Props (factorization for every admissible native cost, and prime-direction propagation from calibration at 2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.