PRCCharacterPrimeWitnessesControlNonunitWitnesses
plain-language theorem explainer
Names the composite bridge for ratio-orbit characters: prime-axis no-mixing implies full nonunit no-mixing. Downstream uniqueness and calibration lemmas cite this Prop when splitting prime witnesses from arbitrary nonunit witnesses. Pure definitional abbreviation of an implication between two existential no-mixing predicates; no proof content.
Claim. For a map $\chi$ on rational orbits, write $P(\chi)$ for the statement that no identity-oriented prime witness coexists with a reciprocal-oriented prime witness, and $N(\chi)$ for the analogous statement over all nonunit orbits. The named property is the implication $P(\chi)\Rightarrow N(\chi)$.
background
In the primitive recognition calculus, a RatioOrbit is a rational display: signed integer numerator over a nonzero distinction-natural denominator. Characters are maps $\chi$ on these orbits. Cost uniqueness work isolates how $\chi$ orients prime directions versus general nonunit directions.
Two existential no-mixing predicates appear. Prime no-mixing says there is no pair of primes where one is identity-oriented under $\chi$ and another is reciprocal-oriented. Nonunit no-mixing is the same ban, but for arbitrary nonunit (non-$±$) orbits rather than primes alone.
The module builds native cost uniqueness from doubled-trace and d'Alembert structure on these characters. After primes are isolated, one still needs a bridge from prime-axis control to full nonunit control; that bridge is exactly this implication.
proof idea
Definitional abbreviation only. The body is the bare implication from prime no-mixing to nonunit no-mixing; no tactics, no lemmas applied. Downstream theorems treat the name as a hypothesis or as one side of an iff with the contrapositive reflection form (mixed nonunit witnesses force mixed prime witnesses).
why it matters
This is the exact composite bridge still needed after prime witnesses are isolated: prime no-mixing must control arbitrary nonunit witnesses. It is the hypothesis of the one-direction theorem that turns control into mixed-nonunit reflection, and the conclusion of the reverse direction from reflection; together those give the iff linking control to reflection.
It is also the payload of the prime-calibration target: under ratio-character and prime-direction calibration hypotheses, one wants this control property for every $\chi$. That target sits on the path toward native cost uniqueness in the PRC stack, which feeds the broader forcing story (J-uniqueness and the recognition composition law) once characters are tied to the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.