PRCPrimeCalibrationForcesNonunitIdentityWitnessExcludesReciprocalTarget
plain-language theorem explainer
Defines the one-sided witness-exclusion target: every prime-direction-calibrated ratio character should make any identity-oriented nonunit witness incompatible with every reciprocal-oriented nonunit witness. Native-cost uniqueness work cites it as a candidate forcing step that strips local orientation from witness globalization. The body is a pure Prop abbreviation (universal quantification over characters), not a proved theorem; downstream material both equates it to a no-mixed-orientation target and refutes it.
Claim. The target proposition asserts: for every map $\chi$ from ratio orbits to ratio orbits that is a PRC ratio character and is prime-direction calibrated, the following holds: if there exists any nonunit identity-oriented orbit witness for $\chi$, then no nonunit reciprocal-oriented orbit witness for $\chi$ can exist.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. A ratio character $\chi$ is a structure-preserving map on those orbits used to read cost and orientation. Prime-direction calibration restricts how $\chi$ treats prime generators, aligning character direction with the native prime ladder.
Identity and reciprocal orientations come from the ledger/observer side: the identity event sits at the J-cost minimum $x=1$, while the reciprocal event swaps source and target and inverts the ratio (the reciprocal automorphism of the cost algebra). A nonunit witness is a non-unit distinction supporting an oriented orbit direction for $\chi$.
The predicate being forced is the one-sided exclusion form of branch coupling: existence of any nonunit identity witness already rules out every nonunit reciprocal witness. Local orientation is deliberately not bundled into that predicate; the target asks whether prime calibration alone yields the exclusion.
proof idea
Definitional Prop, not a proof. The body is the universal closure $\forall,\chi,;\mathrm{RatioCharacter}(\chi)\to\mathrm{PrimeDirectionCalibrated}(\chi)\to\mathrm{IdentityWitnessExcludesReciprocal}(\chi)$. No tactics or lemmas discharge it here; later theorems either transport this target to the no-mixed-orientation target or refute the whole statement.
why it matters
This target is a named blocker fragment in native cost uniqueness. It feeds the Pass-25 blocker certificate structure, which records that native cost uniqueness is not closed and splits the missing mathematics into exact Lean targets. Equivalence theorems identify it with the no-mixed nonunit orbit-orientation target (both directions, and via the no-mixed-witnesses variant), so either form can be used as the globalization step that strips local orientation.
Framework-wise it sits inside the PRC attempt to force the unique native cost compatible with the Recognition Composition Law and J-uniqueness (T5), before phi and the eight-tick constraints enter. Downstream, the target is explicitly refuted: prime calibration does not force one-sided identity-vs-reciprocal witness exclusion. That refutation is itself a certificate input, narrowing which orientation-coupling hypotheses remain viable for uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.