PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget
plain-language theorem explainer
Names the orbit-2 mixed-witness exclusion target: every prime-calibrated ratio character that is reciprocal on the distinguished two-prime axis admits no identity-oriented native prime witness. Cost-uniqueness and character-rigidity arguments cite this Prop as the atomic two-specific blocker. It is a pure definitional packaging of a universal quantification over characters; no proof content.
Claim. The following proposition is the target: for every map $\chi$ on rational orbits that is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and prime-direction calibrated (its generated cost matches canonical $J$-cost on every prime orbit), if $\chi$ sends the orbit-$2$ prime direction to its reciprocal, then no native prime direction is fixed by $\chi$ (no identity-oriented prime witness exists).
background
In the Primitive Recognition Calculus, costs on ratio orbits are candidates for a d'Alembert-style factorization through a ratio character $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$. A RatioOrbit is an integer numerator over a nonzero orbit denominator (K4.7). A ratio character is quotient-native: it preserves the unit and is multiplicative up to cross-equivalence rather than definitional equality.
Prime-direction calibration demands that the cost generated from $\chi$ agrees with the canonical $J$-cost on every prime orbit direction. The atomic obstruction packaged here is the witness form: reciprocal orientation of $\chi$ at the distinguished orbit-$2$ axis cannot coexist with even one identity-oriented native prime witness.
This module isolates exact Lean targets along the native-cost uniqueness route, which ultimately feeds the Recognition forcing chain's $J$-uniqueness (T5) and the Recognition Composition Law.
proof idea
Definitional, not a proved theorem. The body is the universal closure $$\forall\chi,;\mathrm{PRCRatioCharacter},\chi\to\mathrm{PRCCharacterPrimeDirectionCalibrated},\chi\to\mathrm{PRCCharacterTwoPrimeReciprocalExcludesPrimeIdentityWitness},\chi.$$ It simply packages the already-defined witness-level blocker as a single target proposition over all calibrated characters. Downstream lemmas treat inhabitation of this Prop as a hypothesis and discharge mixed-character absurdities by unfolding.
why it matters
This is the atomic two-specific mixed-witness blocker on the character-rigidity path to native cost uniqueness. Downstream, it is equivalent to the non-witness target form and to the "prime-identity forces two-prime-identity" target; inhabiting it immediately yields absurdity of any prime-calibrated mixed character that is reciprocal at orbit 2 and identity at some prime.
It appears in the Pass-25 PRCNativeCostUniquenessBlockerCertificate, which records that native cost uniqueness is not closed but is split into exact Lean targets. In framework terms it supports the route toward unique $J$-cost (T5 / RCL) by ruling out mixed reciprocal/identity orientations on prime axes. Constructing a calibrated mixed-character model would refute the current rigidity route; proving this target advances closure of that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.