PRCCharacterPrimeIdentityWitnessExcludesReciprocal
plain-language theorem explainer
Defines one-sided prime-axis witness exclusion for a ratio-orbit character χ: if any native prime direction is identity-oriented under χ, then no native prime direction may be reciprocal-oriented. Cost-uniqueness and no-mixing arguments cite this as the atomic witness form of prime no-mixing. It is a pure Prop abbreviation, not a proved statement.
Claim. For a map $\chi$ on ratio orbits, the following holds: if there exists a prime distinction $p$ such that $\chi$ sends the prime direction of $p$ to an orbit cross-equivalent to that same prime direction, then for every prime distinction $r$ it is impossible that $\chi$ send the prime direction of $r$ to an orbit cross-equivalent to the reciprocal of that direction.
background
In the Primitive Recognition Calculus, a ratio orbit is a signed-orbit numerator over a nonzero distinction-nat denominator (the internal rational display). Cross-equivalence equates two ratio orbits when scaled numerators balance under the signed-orbit relation; it is the PRC stand-in for rational equality. The total reciprocal on ratio orbits swaps numerator and denominator (sending zero to zero), matching the reciprocal automorphism of the cost algebra and the reciprocal recognition event on the ledger.
A character here is a map $\chi$ on ratio orbits. On a native prime axis (a prime distinction with its prime-orbit certificate), $\chi$ may fix the prime direction up to cross-equivalence (identity orientation) or send it to the reciprocal direction (reciprocal orientation). The surrounding module builds native cost uniqueness from doubled-trace and d'Alembert structure on such characters; prime no-mixing is the constraint that identity and reciprocal orientations cannot both appear among prime axes.
proof idea
No proof: this is a definitional Prop. The body is the implication from an existential identity-oriented prime witness to the universal denial of any reciprocal-oriented prime witness, written with cross-equivalence against the prime direction and against its reciprocal. Downstream lemmas treat the name as a hypothesis or as one side of an iff with global no-mixing predicates.
why it matters
This is the atomic witness packaging of prime no-mixing used throughout native cost uniqueness. Downstream, it is equivalent to no mixed prime orientation and to no mixed prime witnesses (both directions of the iff are proved by unpacking existentials). It feeds the blocker certificate and the prime-calibration target that forces this exclusion. In the Recognition forcing picture, characters that mix identity and reciprocal prime orientations would break the unique J-cost path (T5 J-uniqueness and the Recognition Composition Law); excluding that mix keeps the native cost on the forced branch rather than the reciprocal automorphism branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.