PRCPrimeCalibrationForcesOrbitSuccessorTransportTarget_refuted
plain-language theorem explainer
Prime calibration of a ratio character does not force orbit-identity successor transport in both one-step directions. Native-cost uniqueness and foundation-certificate work cite this as a closed negative. The proof is a short reduction: transport implies the identity-successor target, which is already refuted.
Claim. It is false that every ratio character $\chi$ on ratio orbits which is prime-direction calibrated necessarily satisfies orbit-identity successor transport (both one-step directions separately).
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a multiplicative map on ratio orbits. Prime-direction calibration is a normalization condition along prime orbit directions. The transport target asks that such a calibrated character also respect additive successor steps on nonzero orbit directions in both one-step senses separately.
That target is the sharp directional form of an additive-trace compatibility demand. The module doc line for the target states that it "exposes the exact additive-trace compatibility missing from the purely multiplicative ratio-character laws." A weaker identity-successor target sits downstream of transport: if transport holds for every calibrated character, then the identity-successor property holds as well (via the of-transport implication).
The local setting is native-cost uniqueness: which algebraic laws on characters are forced by calibration hypotheses, and which are not. This declaration closes the transport side of that ledger by refutation.
proof idea
Assume the transport target. Apply PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget_of_transport to obtain the identity-successor target. Discharge by PRCPrimeCalibrationForcesOrbitSuccessorIdentityTarget_refuted, which already shows the identity target is false. Pure reduction along the implication chain; no new counterexample construction at this node.
why it matters
Closes a named negative in the native-cost uniqueness program: prime calibration alone does not buy directional successor transport. That sharpens the gap between multiplicative ratio-character laws and the additive-trace structure needed for a unique native cost.
Downstream it feeds prc_native_cost_uniqueness_blocker_certificate, which packages proved and refuted factorization targets into a single blocker certificate, and appears in the dependency cone of prc_universal_foundation_conditional_certificate. In the Recognition forcing picture this is bookkeeping on the foundation side (what calibration does not force), not a T5–T8 landmark itself; it constrains how far character axioms can be pushed before additive structure must be assumed separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.