PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_of_identity_branch_transport
plain-language theorem explainer
Prime calibration that forces identity-branch transport on nonunit directions also forces witness globalization: any identity-oriented nonunit witness fixes the identity branch globally. Native-cost uniqueness blockers and the universal-foundation conditional certificate cite this implication. The proof is a pointwise lift of the character-level transport-to-globalization lemma under the shared universal quantifiers.
Claim. Assume that whenever a ratio character is prime-direction calibrated, identity orientation on one nonunit direction transports to every nonunit direction. Then, for every such character, any identity-oriented nonunit witness fixes the identity branch on all nonunit directions.
background
In the primitive recognition calculus, a ratio character is a map on ratio orbits that encodes multiplicative orientation data used to build the native cost. Prime-direction calibration restricts how that character may sit on prime generators. Two blocker targets package the same branch-coupling demand under that calibration.
The transport target says: if any nonunit direction remains identity-oriented, that identity branch must carry to every other nonunit direction. The witness-globalization target says: any single identity-oriented nonunit witness already forces the identity branch everywhere on nonunits. At the character level, transport implies globalization by specializing the transported identity to an arbitrary nonunit receiver.
This module develops uniqueness of the native cost (the J-cost shape forced by the Recognition Composition Law) by ruling out mixed-orientation factorizations under prime calibration. The two targets are alternative phrasings of one coupling obstruction in that uniqueness chain.
proof idea
Term-mode, four lines. Introduce a ratio character $\chi$ together with the character and prime-calibration hypotheses. Apply the assumed transport target at $(\chi,h_\chi,h_{\mathrm{prime}})$ to obtain character-level identity-branch transport. Feed that into the upstream lemma that converts character-level branch transport into character-level witness globalization. The result is exactly the witness-globalization target. No extra algebraic work.
why it matters
Closes one direction of the equivalence between the transport and witness-globalization blocker targets, and is the final step in the product-no-mixed route into witness globalization. Downstream, the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate sit on this coupling obstruction: mixed reciprocal/identity orientations on nonunit directions cannot survive prime calibration if either target holds.
In the broader RS forcing picture this is bookkeeping inside native-cost uniqueness (the J-shape $J(x)=(x+x^{-1})/2-1$ from T5 and the RCL), not a new physical constant. It keeps the uniqueness pipeline free of orientation loopholes before cost is promoted into the universal foundation certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.