PRCPrimeFloorSuccessorTransportSharpenedTarget_refuted
plain-language theorem explainer
The Pass-39 sharpened prime-floor successor-transport target is false. Researchers closing false forcing routes in Primitive Recognition Calculus native-cost uniqueness cite this. The target is a conjunction of local nonunit orbit-product orientation with adjacent no-mixing; the proof projects to the first conjunct and applies its prior refutation.
Claim. The sharpened prime-floor successor-transport target fails: it is not the case that prime calibration forces both local nonunit orbit-product orientation and prime-floor absence of adjacent mixed orientation.
background
In the Primitive Recognition Calculus, native-cost uniqueness is attacked by stating candidate forcing targets and either proving or refuting them. Pass 39 refined the prime-floor successor-transport target by splitting a bundled claim into two conjuncts: local nonunit orientation of orbit products under prime calibration, and no adjacent mixed orientation at the prime floor.
The first conjunct already carries an independent refutation upstream (itself a thin wrapper of a still earlier orientation-coherence refutation). The present declaration packages that fact as a refutation of the full sharpened conjunction.
The ambient module develops cost characters, doubled-trace values, and d'Alembert-type identities aimed at pinning the native recognition cost.
proof idea
Short term proof. Assume the sharpened target (a conjunction). Project to the first conjunct via .1. Apply the upstream theorem that already refutes local nonunit orbit-product orientation under prime calibration. The second conjunct is never used.
why it matters
Closes one sharpened false route in the native-cost uniqueness campaign. Downstream consumers include the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate, both of which assemble proved and refuted targets into structured certificates.
In the broader Recognition Science forcing chain, uniqueness of the native cost is the local PRC face of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). Refuting over-strong calibration claims keeps that uniqueness argument from resting on false lemmas. The declaration does not itself prove uniqueness; it only retires a Pass-39 candidate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.