PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_of_nonunit_coherent
plain-language theorem explainer
Under prime direction calibration, global nonunit orbit-orientation coherence implies that any identity-oriented nonunit witness forces the identity branch everywhere. Cost-uniqueness and branch-coupling arguments cite this to equate the two blocker targets. The proof is a one-line pointwise application of the character-level coherence-to-witness-globalization lemma.
Claim. Assume that every ratio-orbit character $\chi$ that is prime-direction calibrated has a single coherent orientation on all nonunit orbit directions. Then every such $\chi$ also satisfies: if any nonunit direction is identity-oriented, that witness forces the identity branch globally on all nonunit directions.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and carry orientation data (identity vs reciprocal) on nonunit directions. Prime-direction calibration is the constraint that $\chi$ respects a preferred prime-axis orientation. Two blocker targets package what calibration should force at the global level.
The stronger target, nonunit orbit-orientation coherence, demands one common orientation across every nonunit direction. The witness-globalization target is the one-sided form: any single identity-oriented nonunit witness already locks the identity branch everywhere. Upstream, the character-level lemma states that coherence alone yields witness globalization, via branch transport: once orientations agree, an identity witness propagates.
This declaration lifts that character fact to the quantified "prime calibration forces ..." targets used by the native-cost uniqueness blocker stack.
proof idea
Term-mode, three steps. Introduce a character $\chi$ together with the ratio-character and prime-calibration hypotheses. Instantiate the assumed coherence target at $(\chi, h_\chi, h_{\mathrm{prime}})$ to obtain nonunit orbit-orientation coherence for $\chi$. Feed that into PRCCharacterNonunitIdentityWitnessGlobalizes_of_coherent, which itself routes through branch transport, and conclude witness globalization for $\chi$. No extra algebraic work.
why it matters
Closes one direction of the equivalence between the two branch-coupling blocker targets: coherence target iff identity-witness-globalization target. That equivalence is the next sibling theorem and is the form the uniqueness stack prefers when swapping formulations.
Downstream it feeds prc_native_cost_uniqueness_blocker_certificate and, through the UniversalFoundation layer, prc_universal_foundation_conditional_certificate. In the Recognition forcing picture this is bookkeeping inside native $J$-cost uniqueness (the T5 J-uniqueness lane): ruling out mixed identity/reciprocal product factors once primes are calibrated, so the cost character cannot split branches. It does not itself force calibration; it only transports one global consequence of calibration into another.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.