Pith. sign in
theorem

PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_of_branch_uniformity

proved
show as:
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
domain
Foundation
line
9860 · github
papers citing
none yet

plain-language theorem explainer

Prime calibration that forces identity-branch uniformity on native prime axes also forces the no-mixed-orientation target: no character may put one prime axis on the identity branch and another on the reciprocal branch. Anyone closing native-cost uniqueness or the branch-uniformity/no-mixing equivalence cites this implication. The proof unpacks the target and applies the character-level uniformity-to-no-mixing lemma.

Claim. Assume that every ratio-orbit character that is prime-direction calibrated is forced to put all native prime axes on the identity branch whenever one of them is identity-oriented. Then every such calibrated character has no mixed prime orientation: it cannot place one native prime axis on the identity branch and another on the reciprocal branch.

background

In the primitive recognition calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative structure is read as cost. Prime-direction calibration means the character respects the preferred orientation on each native prime axis. Two related global targets package what calibration should force.

The branch-uniformity target says: if any native prime axis is identity-oriented under $\chi$, then every native prime axis is on the identity branch. The no-mixed-orientation target says the stronger-looking global prohibition: $\chi$ cannot mix identity and reciprocal choices across different prime axes. At the single-character level, the upstream lemma already shows that identity-branch uniformity implies no mixed prime orientation (by applying uniformity to the identity-oriented witness and contradicting a reciprocal choice on another prime).

This declaration lifts that character-level implication to the two named calibration targets used in the native-cost uniqueness ledger.

proof idea

One-line structural lift. Introduce a character $\chi$ together with the ratio-character and prime-calibration hypotheses of the no-mixing target. Feed those same hypotheses into the assumed branch-uniformity target to obtain identity-branch uniformity for $\chi$. Conclude with the upstream character lemma PRCCharacterNoMixedPrimeOrientation_of_branch_uniform, which turns that uniformity into no mixed prime orientation.

why it matters

Native cost uniqueness in Recognition Science needs prime calibration to pin orientation choices so the cost functional cannot freeload on independent reciprocal flips along different primes. This implication is one half of the proved equivalence between the branch-uniformity target and the no-mixing target, and it is wired into the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate.

In the forcing chain, uniqueness of the $J$-cost (T5) and the Recognition Composition Law require a single coherent reading of multiplicative structure; mixed prime orientations would reopen independent branch choices and block that uniqueness. Closing the equivalence of these two targets shrinks the remaining scaffold surface for PRC native-cost uniqueness to the still-open calibration steps that actually force uniformity (or no-mixing) from the prime data.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.