PRCNativeCostUniquenessSharpenedTarget
plain-language theorem explainer
The sharpened native-cost uniqueness target is the conjunction of two exact blockers: every admissible PRC-native RCL cost factors through a ratio character, and every calibrated rational character cost equals the canonical identity-character cost. Workers on the PRC uniqueness program cite it as the precise interface that replaced the opaque uniqueness blocker. It is pure definitional packaging of those two Props; no proof content.
Claim. The sharpened native-cost uniqueness target is the conjunction of: (i) every $F$ on ratio orbits satisfying the PRC-native cost hypotheses factors as a cost built from some ratio character $\chi$, and (ii) every ratio character $\chi$ whose cost at $2$ matches the canonical on-orbit cost at $2$ has cost equal to the canonical on-orbit cost at every ratio orbit $q$.
background
In the Primitive Recognition Calculus, admissible native costs are maps on ratio orbits obeying the Recognition Composition Law (RCL) and related calibration hypotheses. The classical continuous uniqueness story forces $J(x)=(x+x^{-1})/2-1$ (T5); here the discrete analogue asks whether a PRC-native cost is forced to be the canonical identity-character cost on ratio orbits.
The first conjunct is the discrete d'Alembert factorization step: every admissible native cost $F$ should arise as $\mathrm{costFromCharacter},\chi$ for some ratio character $\chi$. The second conjunct is rigidity: once a character cost is calibrated at $2$ against the canonical on-orbit cost, prime-direction freedom is eliminated and the character cost equals the canonical cost everywhere.
This definition packages those two Props as the sharpened replacement for an earlier opaque native uniqueness blocker in the same module.
proof idea
Definitional conjunction only. The body is the logical and of the factorization target and the rigidity target; there is no tactic proof and no lemma application beyond naming those two Props.
why it matters
It is the Pass-era sharpening of the native uniqueness interface: instead of one opaque blocker, uniqueness is split into factorization plus rigidity. Downstream, the blocker certificate records that native cost uniqueness is not closed but is now stated as exact Lean targets. The companion theorem immediately refutes this sharpened target by refuting its first conjunct (factorization), so the route cannot force the final uniqueness surface as written.
The same package appears in the universal-foundation open-target ledger, which tracks proved repaired interfaces against exact refutations. Framework-wise this sits under the discrete side of T5 J-uniqueness and RCL: the continuous $J$ is unique, but the PRC-native discrete packaging needed a sharper, and ultimately refutable, factorization claim before a repaired zero-calibrated route could be isolated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.