PRCPrimeCalibrationForcesPrimeFloorIdentitySuccessorStepPairTarget_refuted
plain-language theorem explainer
The split one-step prime-floor successor target is false: prime calibration does not force both the extend and contract successor-step identities at once. Anyone tracking native-cost uniqueness blockers or the PRC universal-foundation certificate cites this. The proof is a short transport: the step-pair form is equivalent to the successor-transport target, already refuted.
Claim. It is not the case that prime calibration forces both halves of the corrected prime-floor successor package at once: the identity does not simultaneously extend and contract along every successor step in the required sense. Equivalently, the conjunction of the extend-successor-step target and the contract-successor-step target fails.
background
In the Primitive Recognition Calculus, native cost uniqueness is obstructed by several candidate "forcing" targets that would pin the cost character from prime calibration alone. The prime-floor successor package is one such candidate: it asks that calibration on primes orient the identity along successor steps of nonunit orbits, not only along prime axes.
The split one-step form packages that demand as a conjunction: an extend-successor-step clause and a contract-successor-step clause. Upstream, that conjunction is proved equivalent to a single successor-transport target (the iff between transport and step-pair forms). The transport target itself is already refuted by reduction to a still stronger globalization claim (prime-identity witness globalizes every nonunit direction), which fails.
Local setting is the PRC native-cost uniqueness module: J-cost characters, doubled-trace d'Alembert structure, and calibration hypotheses that try to force a unique native cost from prime data.
proof idea
Term-mode reductio in three steps. Assume the step-pair target. Apply the reverse direction of the equivalence successor transport ↔ successor step-pair to obtain the successor-transport target. Discharge by the already-proved refutation of that transport target (itself reduced upstream to failure of prime-identity witness globalization on nonunits). No new arithmetic; pure propositional transport along the iff.
why it matters
Closes one concrete false branch in the prime-floor successor blocker family. Downstream it is consumed by prc_native_cost_uniqueness_blocker_certificate, which assembles proved and refuted factorization targets into a single uniqueness-blocker record, and by prc_universal_foundation_conditional_certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic certificates under the conditional foundation story.
In framework terms this sits under the PRC foundation layer that feeds the forcing chain (T5 J-uniqueness and the Recognition Composition Law for the cost), not a direct T0–T8 step. It records that prime-axis calibration alone does not force the full successor-step identity package, so native-cost uniqueness must route through other proved targets (e.g. zero-calibrated factorization) rather than this refuted path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.