PRCPrimeCalibrationForcesNonunitIdentityWitnessLocalExclusionTarget_refuted
plain-language theorem explainer
Under prime calibration, the local split of identity-witness globalization (local nonunit-orbit orientation plus one-sided reciprocal-witness exclusion) is false. Native-cost uniqueness and universal-foundation certificates cite this refutation as a closed blocker. The proof transfers the already-refuted global witness-globalization target across a proved equivalence.
Claim. The conjunction of (i) local orientation of the nonunit orbit under prime calibration and (ii) one-sided exclusion of the reciprocal identity witness is false: that local-exclusion package does not hold.
background
In the Primitive Recognition Calculus, native cost uniqueness is attacked by factoring cost characters and tracking how identity witnesses move on nonunit orbits under prime calibration. Witness globalization asks that a reciprocal orientation fixed at one nonunit direction transport to every nonunit direction.
The local-exclusion target is the split form of that demand: local orbit orientation conjoined with one-sided exclusion of the reciprocal identity witness. An upstream equivalence identifies this split with the global witness-globalization target, and that global target is already refuted by reduction to a failed identity-branch transport claim.
The ambient module builds the uniqueness and blocker stack for native costs (J-cost characters, doubled-trace d'Alembert structure, and calibration constraints) before packaging certificates for the universal foundation layer.
proof idea
Assume the local-exclusion target. Apply the right-to-left direction of the proved equivalence between witness globalization and local exclusion to obtain the global witness-globalization target. Discharge the goal by the already-proved refutation of that global target (itself reduced earlier to a failed identity-branch transport). Pure modus-tollens transfer; no new analytic work.
why it matters
Closes the local half of the identity-witness globalization fork in the native-cost uniqueness blocker stack. Downstream, prc_native_cost_uniqueness_blocker_certificate aggregates proved factorizations and refuted signed-admissible paths; this refutation keeps the local-exclusion branch from reopening a nonunit identity loophole. The same blocker feeds prc_universal_foundation_conditional_certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic certificates. In the broader RS forcing picture this is bookkeeping on the cost side of T5 J-uniqueness and the Recognition Composition Law: it rules out a calibration path that would let a nonunit identity witness survive locally without global transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.