PRCCharacterSamePrimeMixedPairWitnesses
plain-language theorem explainer
Defines the same-axis mixed-prime pair witness property for a ratio-orbit character χ: some native prime orbit simultaneously carries both an identity-oriented and a reciprocal-oriented prime witness under χ. This is the self-reciprocal branch-conflict case used when splitting mixed-prime pair witnesses. The body is a pure existential Prop over prime orbits and cross-equality; no proof content.
Claim. A map $\chi$ from ratio orbits to ratio orbits has a same-axis mixed-prime pair witness when there exists a native prime orbit $p$ such that $\chi$ sends the prime direction of $p$ to a ratio orbit cross-equivalent to that same prime direction, and also sends it to a ratio orbit cross-equivalent to the reciprocal of that prime direction (equivalently: two prime labels $p=r$ witness identity orientation and reciprocal orientation together).
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit displays: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are identified by cross-equality (crossEq), the internal PRC stand-in for rational equality via balanced scaled numerators. Reciprocation of a ratio orbit flips the displayed ratio; identity orientation keeps the prime direction fixed.
A character $\chi$ is a self-map of ratio orbits used to read cost-like structure off prime directions. Mixed-prime pair witnesses ask whether $\chi$ can simultaneously realize an identity-oriented prime witness and a reciprocal-oriented prime witness. The same-axis case forces those two witnesses onto one and the same native prime orbit ($p=r$), which is the self-reciprocal branch-conflict configuration named in the doc-comment.
Upstream ledger and cost algebra supply the reciprocal automorphism and the identity event at the $J$-cost minimum ($x=1$). Here those ideas appear only through orbit-level recip and cross-equality on prime directions.
proof idea
Definitional Prop, not a proved theorem. The body packages three conjuncts inside nested existentials: prime-orbit data for labels $p$ and $r$, the equality $p=r$, cross-equality of $\chi$ on the prime direction of $p$ with that same prime direction, and cross-equality of $\chi$ on the prime direction of $r$ with the reciprocal of that direction. No tactics or lemmas are applied; downstream theorems unpack the package with rcases and subst.
why it matters
This predicate is the same-orbit half of the mixed-prime witness dichotomy. Downstream, mixed-prime pair witnesses are equivalent to the disjunction of same-axis and distinct-axis forms (PRCCharacterMixedPrimePairWitnesses_iff_same_or_distinct and the of-same / same-or-distinct introduction and elimination lemmas). The companion absurdity theorem PRCCharacterSamePrimeMixedPairWitnesses_absurd shows the same-axis case never occurs, so absence of mixed-prime witnesses reduces to ruling out the distinct-axis branch alone (PRCCharacterNoMixedPrimeWitnesses_iff_no_same_and_no_distinct_pair).
That cleanup feeds prime-calibrated character uniqueness (PRCPrimeCalibratedSamePrimeMixedPairWitnessCharacter) and is listed among universal-foundation open targets. In the broader RS forcing picture it polices self-reciprocal conflicts on prime directions before native cost can be identified with the unique $J$-cost (T5) along the recognition composition law, keeping characters free of identity/reciprocal double-booking on a single prime axis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.