PRCPrimeCalibrationForcesNoDistinctPrimePairWitnessCharacter_of_prime_identity_branch_uniformity
plain-language theorem explainer
If prime calibration forces identity-branch uniformity on every calibrated ratio character, then no calibrated character can witness a mixed branch between two distinct native prime orbits. Cost-uniqueness and foundation-certificate arguments cite this as one direction of the uniformity/no-mixed-pair equivalence. The proof unpacks an existential witness and feeds it to the per-character absurdity lemma.
Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated is identity-branch uniform on native prime axes. Then there is no ratio character that is simultaneously a ratio character, prime-direction calibrated, and a witness that a mixed branch occurs between two distinct native prime orbits.
background
In the Primitive Recognition Calculus, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode how recognition cost orients along ratio orbits. Prime-direction calibration means the character respects the preferred orientation on native prime axes. Identity-branch uniformity says that once any native prime axis sits on the identity branch, every native prime axis does.
The branch-uniformity target packages that implication globally: prime calibration should force identity-branch uniformity for every such character. The opposing model is a calibrated distinct-axis mixed-prime pair witness: some calibrated character places a mixed branch between two different native prime orbits.
Upstream, the per-character lemma already shows that identity-branch uniformity on a fixed $\chi$ rules out distinct-prime mixed-pair witnesses for that same $\chi$. This declaration lifts that local absurdity to the global target-versus-existence level.
proof idea
Term-mode proof by contradiction. Introduce a hypothetical calibrated distinct-prime mixed-pair witness character and unpack the existential as $\langle \chi, h_\chi, h_{\mathrm{prime}}, h_{\mathrm{charDistinct}} \rangle$. Apply the uniformity target hypothesis at that $\chi$ (using the ratio-character and prime-calibration facts) to obtain identity-branch uniformity for $\chi$. Discharge the goal by the upstream lemma that identity-branch uniformity makes distinct-prime mixed-pair witnesses absurd on that character.
why it matters
This is one half of the equivalence between the prime-identity branch-uniformity target and the non-existence of calibrated distinct-prime mixed-pair witnesses. Downstream, the biconditional and its negated form both cite it, packaging the target as a clean obstruction statement.
That obstruction feeds the conditional universal-foundation certificate in UniversalFoundation, which assembles kernel, real-field, and trace-logic certificates under named hypotheses. In the Recognition forcing picture, ruling out mixed branches on distinct prime axes is part of locking native cost structure before J-uniqueness (T5) and the self-similar fixed point $\phi$ (T6) are used at the continuum level. The declaration itself is fully proved; it does not close the target, only converts it into a no-witness claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.