PRCNativeCostCharacterRigiditySharpenedTarget_refuted
plain-language theorem explainer
The sharpened native-cost character-rigidity target is false: it cannot hold as a conjunction. Anyone tracking PRC uniqueness blockers or Pass-26 rigidity refinements would cite this. The proof is a one-line projection: the first conjunct (two-calibration forces prime calibration) is already refuted, so the whole target fails.
Claim. The sharpened rigidity target is false: it is not the case that both (i) every two-calibration of a native-cost ratio character forces prime calibration and (ii) prime calibration propagates as required by the Pass-26 refinement.
background
In the Primitive Recognition Calculus, native cost is recovered from ratio characters via a doubled-trace / d'Alembert route tied to the J-cost $J(x)=(x+x^{-1})/2-1$. Uniqueness programs ask whether calibration hypotheses pin the character (hence the cost) down to the intended PRC form.
The sharpened rigidity target is a Pass-26 refinement: the conjunction of "two calibrations force prime calibration" and a prime-calibration propagation clause. The first conjunct is already known false: there is a concrete ratio character (the three-to-five rebase character) that meets the two-calibration hypotheses yet fails to be three-prime-calibrated.
This module records which candidate uniqueness targets survive and which are blockers. Refuting the sharpened conjunction keeps the uniqueness ledger honest before any universal-foundation packaging.
proof idea
Term-mode one-liner after intro. Assume the sharpened target; project to its first conjunct (two-calibration forces prime calibration); discharge by the existing refutation of that conjunct. The second conjunct is never inspected: falsity of one factor kills the conjunction.
why it matters
Closes a Pass-26 rigidity candidate that would otherwise look like a uniqueness route for native cost from character data. Feeds prc_native_cost_uniqueness_blocker_certificate, which aggregates proved factorizations against refuted over-strong targets, and is visible to prc_universal_foundation_conditional_certificate in the universal-foundation layer.
In the broader RS forcing picture this is bookkeeping on the cost side of T5 (J-uniqueness) and the Recognition Composition Law: it does not replace J-uniqueness, but prevents an overstated calibration-to-character implication from being treated as proved. The open path remains whatever weaker, still-open uniqueness or factorization targets the blocker certificate leaves standing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.