PRCPrimeCalibrationForcesNonunitIdentityWitnessGlobalizesTarget_of_product_no_mixed
plain-language theorem explainer
Assuming prime calibration rules out mixed identity/reciprocal orientations on orbit products, any identity-oriented nonunit direction forces the identity branch globally. Native-cost uniqueness and the product-no-mix ↔ witness-globalization equivalence cite this bridge. The proof is a two-step term composition through the identity branch-transport target.
Claim. If prime calibration forces every ratio character to have no mixed identity/reciprocal factor orientations under native orbit multiplication, then prime calibration also forces the following: whenever a ratio character admits any identity-oriented nonunit direction, that witness fixes the identity branch globally.
background
In the primitive recognition calculus, ratio characters $\chi$ assign orbit data on the ratio lattice. Prime-direction calibration constrains how $\chi$ behaves on prime generators. Two blocker targets package the same orientation rigidity in different forms.
The product no-mixing target asserts that, under prime calibration, native multiplication never mixes identity-oriented and reciprocal-oriented nonunit factors. The witness-globalization target is the branch-coupling form: if any identity-oriented nonunit direction is allowed, that single witness forces the identity branch on every nonunit direction.
Upstream, product no-mixing already yields coherent nonunit orientation and then identity branch transport. A separate lemma turns branch transport into witness globalization by applying the character-level transport-to-globalization map at each calibrated $\chi$.
proof idea
Term-mode composition, not a tactic script. First apply the upstream theorem that product no-mixing implies the identity branch-transport target (itself via coherent orientation). Feed that hypothesis into the one-line wrapper that converts branch transport into witness globalization: introduce $\chi$, character, and prime-calibration hypotheses, then invoke the character-level lemma that branch transport yields nonunit identity witness globalization.
why it matters
Closes one direction of the equivalence between product no-mixing and identity witness globalization under prime calibration; the converse is the sibling implication. That equivalence is the orientation-rigidity hinge inside native-cost uniqueness: mixed product factors are incompatible with a single global identity branch once nonunit directions are non-self-reciprocal.
Downstream it appears in the native-cost uniqueness blocker certificate pathway and in the conditional universal-foundation certificate that packages kernel, ordered-field, and trace-logic ingredients. In the broader Recognition forcing picture this is foundation plumbing for unique native cost (the $J$-cost side of T5), not a direct derivation of $\phi$, the eight-tick period, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.