PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_of_character_factorization
plain-language theorem explainer
From the discrete d'Alembert factorization hypothesis (every admissible native RCL cost factors through a ratio character), uniqueness of the prime-signed strengthened native cost follows: any such F agrees with the canonical on-orbit cost. Anyone closing native-cost uniqueness after the sign and prime-axis repairs would cite this bridge. The proof is a pure term composition through one signed-admissible intermediate.
Claim. Assume every admissible PRC-native RCL cost $F$ factors through some ratio character $\chi$ (discrete d'Alembert factorization). Then every $F$ satisfying the prime-signed strengthened native-cost hypotheses is unique: for all ratio orbits $q$, $F(q)$ is cross-equal to the canonical on-orbit cost.
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits obeying the Recognition Composition Law (RCL) and related admissibility axioms. The first exact blocker in the uniqueness program is the discrete d'Alembert factorization: every admissible native cost should factor as a cost built from a ratio character $\chi$, written $\mathrm{crossEq}(F(q),\mathrm{costFromCharacter}(\chi,q))$.
After two no-go repairs (sign calibration and prime-axis calibration), the strengthened uniqueness target asserts that any $F$ meeting the prime-signed strengthened hypotheses agrees with the canonical on-orbit cost on every orbit. The local module packages these targets as propositions and chains implications among them.
Upstream, the character-factorization target is the hypothesis interface for the factorization step; a sibling theorem lifts it to a signed-admissible factorization target, and another discharges uniqueness from that intermediate.
proof idea
Pure term-mode composition, no tactics. First apply the sibling that turns the plain character-factorization hypothesis into the signed-admissible character-factorization target (unpacking strengthened native hypotheses, extracting $\chi$, and checking prime/sign admissibility). Feed that result into the one-step uniqueness lemma from signed-admissible factorization, which unpacks $\chi$, uses the pointwise crossEq match to the character cost, and transits to the canonical on-orbit cost.
why it matters
This is the clean entry point from the discrete d'Alembert factorization blocker to the repaired native-cost uniqueness target (sign and every prime axis calibrated). It sits in the PRC native-cost uniqueness spine that underwrites J-uniqueness (forcing chain T5): once costs factor through characters and the strengthened hypotheses hold, the cost is forced to the canonical orbit representative tied to $J(x)=(x+x^{-1})/2-1$. No downstream users are wired yet in the graph; the declaration exists to close the implication chain so later global uniqueness theorems can assume only the factorization target rather than the full signed-admissible package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.