PRCPrimeCalibrationForcesPrimeIdentityWitnessGlobalizesNonunitTarget_of_no_mixed_prime_witnesses
plain-language theorem explainer
Under prime calibration, forbidding mixed prime witnesses forces any identity-oriented prime witness to globalize to every nonunit orbit direction. Native-cost uniqueness and the universal-foundation certificate cite this implication. The proof is a short term application of the character-level globalization lemma, supplying proved orbit-product compatibility and local prime orientation.
Claim. Assume that every prime-direction-calibrated ratio character has no mixed prime witnesses. Then every such character also satisfies the witness-globalized prime-floor property: if any calibrated prime axis picks the identity orientation, every nonunit orbit direction picks identity.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how a candidate native cost orients multiplicative structure. Prime-direction calibration means $\chi$ is constrained on prime axes so that each prime direction is assigned a coherent orientation (identity versus reciprocal).
No-mixed prime witnesses is the existential exclusion: once an identity-oriented prime witness exists, no reciprocal-oriented prime witness is allowed on any prime axis. The target proved here is the witness-globalized prime-floor blocker: identity on any calibrated prime axis forces identity on every nonunit orbit direction.
Upstream, the character-level lemma already shows that orbit-product display compatibility, local prime orientation, and no-mixed witnesses together imply nonunit globalization for a fixed $\chi$. Separate proved targets supply compatibility and local orientation for every calibrated character; the remaining hypothesis is the no-mixed target.
proof idea
Term-mode proof. Introduce a ratio character $\chi$ with the ratio-character and prime-calibration hypotheses. Apply the character-level theorem that no-mixed witnesses plus compatibility and local orientation yield nonunit identity globalization. Feed three ingredients: the proved orbit-product display compatibility target at $\chi$, the proved local prime-orientation target at $\chi$, and the no-mixed hypothesis specialized at $\chi$. No further case analysis.
why it matters
This is the forward half of the corrected prime-floor successor target: it converts the existential no-mixed witness condition into the globalized identity-on-nonunits blocker used in native-cost uniqueness. Downstream it pairs with the converse to give an iff between the two targets, and it is assembled into the native-cost uniqueness blocker certificate. That certificate, in turn, is consumed by the universal-foundation conditional certificate in the PRC foundation stack.
In Recognition Science terms, the step tightens uniqueness of the native cost functional before J-uniqueness (T5) and the RCL are fully locked: mixed prime orientations would leave a residual discrete ambiguity on the prime floor; ruling them out forces a single global identity orientation on nonunits. It does not itself derive $J$ or $\phi$, but clears a discrete obstruction on the path to those forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.