PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_of_local_exclusion
plain-language theorem explainer
If prime calibration already forces local nonunit orbit orientation and one-sided exclusion of reciprocal identity witnesses, then any identity-oriented nonunit witness globalizes the identity branch. Cited by the native-cost uniqueness blocker certificate and the local/global iff. Proof is a short intro that projects the conjunction and applies the character-level globalization lemma.
Claim. Assume the split target: under prime direction calibration, every ratio character has locally oriented nonunit orbits, and every identity-oriented nonunit witness excludes all reciprocal-oriented nonunit witnesses. Then the global target holds: for every ratio character $\chi$ that is prime-direction calibrated, any identity-oriented nonunit witness for $\chi$ forces the identity branch on every nonunit direction.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode multiplicative branch data on ratio orbits. Prime-direction calibration restricts how $\chi$ may act on prime generators. Nonunit directions are orbits away from the unit class; an identity-oriented witness is a nonunit direction on which $\chi$ selects the identity branch rather than the reciprocal branch.
Witness globalization says that a single identity-oriented nonunit witness, once allowed by prime calibration, fixes the identity branch on every nonunit direction. The local-exclusion package splits that demand into two pieces: local orientation of nonunit orbits, plus one-sided incompatibility between any identity-oriented witness and every reciprocal-oriented witness. The module treats these as equivalent blocker forms for branch coupling in the native cost uniqueness argument.
Upstream, the character-level lemma already shows that local orientation plus reciprocal exclusion imply globalization for a fixed $\chi$. The targets here quantify that implication over all prime-calibrated ratio characters.
proof idea
Term-style tactic proof. Introduce a ratio character $\chi$ together with the ratio-character and prime-calibration hypotheses. Project the assumed local-exclusion target conjunction: the first component supplies local nonunit orbit orientation for $\chi$, the second supplies one-sided reciprocal witness exclusion for $\chi$. Feed both into PRCCharacterNonunitIdentityWitnessGlobalizes_of_local_excludes, which returns globalization for that $\chi$. No further case analysis.
why it matters
Closes one direction of the equivalence between the global witness-globalization blocker and its split local-exclusion form. That equivalence is recorded immediately downstream as the iff theorem pairing this result with the converse. The native-cost uniqueness blocker certificate consumes this family of targets when assembling the certificate that zero-calibrated native-cost character factorizations are forced and signed-admissible alternatives are refuted. The same material feeds the conditional universal-foundation certificate in UniversalFoundation, tying PRC kernel, ordered-field, and trace-logic passes together. In the broader Recognition forcing picture this is bookkeeping on branch coupling for the native $J$-cost uniqueness path (T5-adjacent), not a new physical constant derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.