PRCPrimeCalibratedMixedPrimePairWitnessCharacter_same_or_distinct
plain-language theorem explainer
Any prime-calibrated mixed-prime pair witness on a ratio character splits into a same-axis case or a distinct-axis case. Cost-uniqueness and foundation auditors cite this when discharging the mixed-pair obstruction under calibration. The proof unpacks the existential package and reapplies the uncalibrated character-level dichotomy.
Claim. Suppose there is a ratio-orbit character $\chi$ that is prime-direction calibrated and admits a mixed-prime pair witness (an identity-oriented native prime axis $p$ and a reciprocal-oriented native prime axis $r$). Then either the mixed branch occurs on a single native prime orbit, or it occurs between two distinct native prime orbits.
background
In the Primitive Recognition Calculus, a ratio character is a map $\chi$ on ratio orbits that encodes how multiplicative structure is read by the native cost. Prime-direction calibration fixes preferred identity and reciprocal orientations along native prime axes, so the mixed-pair data are not free packaging: $p$ is identity-oriented and $r$ is reciprocal-oriented.
A mixed-prime pair witness asserts that both orientations appear in the character data. That witness may place $p$ and $r$ on the same native prime orbit or on two different ones. The uncalibrated dichotomy already states that any mixed-pair witness on a fixed $\chi$ is same-axis or distinct-axis.
This module packages those witnesses together with calibration into three propositions: the mixed model, the same-prime calibrated model, and the distinct-prime calibrated model. The present result lifts the character-level split to that calibrated packaging.
proof idea
Unpack the hypothesis to a character $\chi$ with ratio-character, prime-direction calibration, and mixed-pair witness data. Apply the upstream character-level split PRCCharacterMixedPrimePairWitnesses_same_or_distinct to that witness. On the left branch, repackage $\chi$ with the same-prime mixed witnesses into the calibrated same-axis proposition; on the right branch, repackage into the calibrated distinct-axis proposition. No new arithmetic is performed.
why it matters
This is one direction of the calibrated mixed-pair biconditional: mixed calibrated data are equivalent to the disjunction of same-axis and distinct-axis calibrated models. That biconditional is the clean interface used when the mixed-pair obstruction is case-split in native-cost uniqueness arguments.
Downstream it is consumed by the universal-foundation conditional certificate, which assembles kernel, real-complete ordered field, and trace-logic passes into a single foundation bundle. In the Recognition forcing picture this sits under native cost uniqueness for the J-cost (T5), before phi and the octave constraints are forced: the mixed-pair geometry of prime axes must be reduced to exclusive same-versus-distinct cases before cost uniqueness can close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.