PRCNativeCostUniquenessSharpenedTarget_refuted
plain-language theorem explainer
The sharpened native-cost uniqueness target is false: the conjunction of character factorization and character rigidity cannot hold. Foundation workers closing the PRC uniqueness blocker cite this to retire the Pass-26 sharpened formulation. The argument is a one-line projection onto the already-refuted factorization conjunct.
Claim. The conjunction of the native-cost character-factorization target and the native-cost character-rigidity target is false.
background
In the Primitive Recognition Calculus, native cost uniqueness asks whether the recognition cost on positive reals is forced once a short list of structural hypotheses is fixed. The opaque uniqueness blocker was replaced by a sharpened target: the conjunction of a character-factorization claim and a character-rigidity claim.
Character factorization asserts that the native cost factors through a ratio character in a prescribed way; character rigidity asks that any such character be forced to the standard logarithmic form tied to the J-cost $J(x)=(x+x^{-1})/2-1$. The factorization half was already refuted upstream by reducing it to a failed trace-lift target.
Local setting is the PRC native-cost uniqueness module, which packages these targets and their refutations as certificates for the broader foundation stack.
proof idea
Assume the sharpened target. Project to its first conjunct (character factorization). Discharge by the existing theorem that the factorization target is false, which itself routes through the trace-lift refutation. No separate work on the rigidity conjunct is required.
why it matters
Closes the Pass-26 sharpened replacement for the opaque native uniqueness blocker. Downstream it feeds the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate, so the foundation stack can record that this particular uniqueness packaging is dead.
In the broader Recognition Science chain this sits next to T5 J-uniqueness: the classical cost $J$ is unique under the Recognition Composition Law, but the native PRC packaging attempted here does not survive in sharpened form. The result clears a false path rather than proving a positive uniqueness theorem; positive uniqueness continues through other calibrated routes in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.