PRCPrimeCalibrationPropagationTarget_refuted
plain-language theorem explainer
Prime-direction calibration of a ratio character does not force the character cost to match the native cost on every rational direction. Anyone auditing uniqueness of the PRC native cost cites this negative result. The proof is a short reduction: the propagation claim implies prime-pair product cost consistency, already refuted.
Claim. It is false that every ratio-orbit character $\chi$ calibrated on all prime directions satisfies $\mathrm{cost}_\chi(q)\simeq C(q)$ (cross-equality of character cost with the native cost) for every rational direction $q$. Equivalently: prime calibration does not propagate the native cost across the full rational orbit lattice by unique factorization alone.
background
In the Primitive Recognition Calculus, costs live on ratio orbits. A ratio character $\chi$ is a multiplicative map on those orbits; its induced cost is built by reading $\chi$ against the native cost functional. Prime-direction calibration means that on every prime generator the character cost already agrees with the native cost (cross-equality).
The propagation target ("sharper target B") asserts the unique-factorization side of rigidity: once every prime direction is calibrated, the character cost should match the native cost on every rational direction. That is the natural hope if multiplicative structure alone pinned the cost.
An upstream implication shows that full propagation forces a weaker statement: consistency of character cost on products of two prime directions. That weaker prime-pair product consistency target has already been refuted in this module, so the stronger propagation claim cannot hold either.
proof idea
Term-mode reductio. Assume the propagation target. Specialize it, via the upstream implication lemma, to the product of two prime directions; that yields the prime-pair product cost-consistency target. Discharge by the already-proved refutation of that consistency target. No new analytic work: pure logical chaining of two prior results.
why it matters
Closes the unique-factorization route to native-cost uniqueness: calibrating primes is not enough to force the cost on all rationals. Downstream, the same refutation underwrites the global-orientation and sharpened-propagation refutations (both reduce to this one), and it is recorded in the native-cost uniqueness blocker certificate. That blocker feeds the conditional universal-foundation certificate, marking which rigidity paths are dead ends versus still open. In the broader RS forcing picture this is local bookkeeping on cost uniqueness, not a T5–T8 landmark, but it prevents a false shortcut to J-cost uniqueness via prime factorization alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.