PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_iff_local_exclusion
plain-language theorem explainer
Prime calibration's branch-coupling blocker has two equivalent shapes: a global form (any identity-oriented nonunit witness fixes the identity branch everywhere) and a split form (local orientation plus one-sided exclusion of reciprocal witnesses). Anyone transferring a refutation or certificate between those shapes cites this. The proof is the term-mode pair of the two already-proved one-way implications.
Claim. Under the primitive recognition calculus, the following are equivalent: (i) every prime-calibrated ratio character that admits an identity-oriented nonunit witness has that witness globalize the identity branch; (ii) prime calibration forces both local nonunit-orbit orientation and one-sided exclusion of every reciprocal-oriented nonunit witness.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode admissible cost-like data. Prime-direction calibration restricts how $\chi$ may treat prime generators. A nonunit identity witness is an identity-oriented direction away from the unit orbit; globalization says that one such witness locks the identity branch on every nonunit orbit.
The local-exclusion target splits that demand: local orientation of nonunit orbits, plus a one-sided rule that an identity-oriented witness excludes every reciprocal-oriented witness. The module develops native-cost uniqueness blockers; these two Props are alternate packagings of the same branch-coupling obstruction under prime calibration.
Upstream, each direction of the equivalence is already a theorem: local exclusion implies globalization, and globalization implies the split (via orientation coherence extracted from the global witness).
proof idea
Term-mode Iff constructor. Left-to-right applies the theorem that globalization yields local exclusion (which unpacks orientation coherence then the conjunction). Right-to-left applies the theorem that local exclusion yields globalization, which introduces a calibrated character and invokes the local-excludes-to-globalizes lemma on witnesses. No new calculus; pure packaging of the two one-way results.
why it matters
This bridge lets the development refute either packaging and transport the negation. Downstream, the local-exclusion target is refuted by reducing through this iff to the already-refuted globalization target. That refutation feeds prc_native_cost_uniqueness_blocker_certificate, which records which factorization and signed-admissible routes are closed. The same equivalence is consumed by the universal-foundation conditional certificate, tying the PRC native-cost uniqueness blockers into the broader foundation stack.
In Recognition Science terms this sits inside the cost-uniqueness forcing that supports J-uniqueness (T5) and the Recognition Composition Law: branch-coupling blockers constrain which characters can pretend to be native costs. The declaration itself does not close uniqueness; it only equates two blocker interfaces so certificates and refutations stay aligned.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.