PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_of_coherent
plain-language theorem explainer
Prime-calibration coherence of nonunit orbit orientations implies the identity-branch transport target: any identity-oriented nonunit direction forces the identity branch on every nonunit direction. Cited by the native-cost uniqueness blocker certificate and by the product-no-mixed reduction path. Proof is a pointwise application of the character-level coherence-to-transport 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$ satisfies identity-branch transport: if any nonunit direction is identity-oriented, the identity branch extends to every nonunit direction.
background
In the Primitive Recognition Calculus, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode how multiplicative structure is read on orbits. Prime-direction calibration restricts how $\chi$ acts on prime generators. Nonunit directions may be identity-oriented or reciprocal-oriented; coherence means a single global choice across all nonunit orbits.
The coherent-orientation target asserts that prime calibration forces that global choice. The identity-branch transport target is the positive transport form of the same branch-coupling blocker: one identity-oriented nonunit witness must fix the identity branch everywhere. The module develops native-cost uniqueness by ruling out mixed orientation factorizations that would produce non-unique costs.
Upstream, the character-level lemma already shows that orbit-orientation coherence of a fixed $\chi$ yields identity-branch transport for that $\chi$. The present statement lifts that implication from characters to the quantified prime-calibration targets.
proof idea
Term-mode one-line wrapper. Introduce a character $\chi$ together with the ratio-character and prime-calibration hypotheses. Apply the coherent-orientation target hypothesis at $(\chi, h_\chi, h_{\mathrm{prime}})$ to obtain character-level coherence, then feed that into the upstream lemma that coherence implies identity-branch transport. No further case analysis.
why it matters
Closes the coherent-to-transport arrow in the branch-coupling blocker stack for native-cost uniqueness. Downstream, the product-no-mixed path reduces through this theorem: product no-mixed orientation yields coherence, which yields transport. The uniqueness blocker certificate assembles these targets among the certified obstacles to non-unique native costs.
In the broader Recognition forcing chain, native cost uniqueness supports the J-cost identification (T5) and the Recognition Composition Law, by ensuring the cost functional read from characters is forced rather than branched. Without transport of the identity branch, mixed reciprocal factors could survive prime calibration and split the cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.