PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget_of_two_prime_reciprocal_excludes_witness
plain-language theorem explainer
If every prime-calibrated ratio character that puts the orbit-2 axis on the reciprocal branch admits no identity-oriented native prime witness, then prime calibration forces identity on orbit 2 whenever any calibrated prime axis is identity-oriented. Native-cost uniqueness and coherent-orientation arguments cite this bridge. The proof is a two-step term composition through the non-witness exclusion target.
Claim. Assume that for every ratio character $\chi$ that is prime-direction calibrated, if the orbit-$2$ prime axis is reciprocal-oriented then no identity-oriented native prime witness exists. Then, for every such $\chi$, identity orientation on any calibrated prime axis forces identity orientation on the orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how multiplicative structure is read by the native cost. Prime-direction calibration fixes the orientation of each prime axis to one of two branches: identity or reciprocal. Orbit $2$ is the distinguished even prime axis; its orientation is the one-sided control that later forces coherent orientation across all primes.
The hypothesis is the two-specific mixed-witness exclusion target: whenever calibration leaves orbit $2$ reciprocal, no native prime may still sit on the identity branch as a witness. The conclusion is the one-sided distinguished-axis target: identity at any calibrated prime forces identity at orbit $2$. Both are pure Prop packages over calibrated characters; neither yet asserts uniqueness of the native cost $J$.
Upstream, the non-witness form of reciprocal exclusion already implies the ordinary reciprocal-exclusion target, and that target already implies the identity-forces-two target. This declaration only packages the witness-level hypothesis into the same conclusion.
proof idea
Term-mode composition of two already-proved bridges. First apply the witness-to-target lemma: the mixed-witness exclusion hypothesis yields the ordinary two-prime reciprocal exclusion target (for each calibrated character, reciprocal orbit $2$ excludes any identity-oriented native prime). Then feed that into the reciprocal-exclusion-to-identity-forces lemma, which rewrites the exclusion as the one-sided force: identity on any calibrated prime implies identity on orbit $2$. No new character arithmetic is performed here.
why it matters
This is the witness-level half of the equivalence between the identity-forces-two target and the mixed-witness reciprocal exclusion. Downstream, that equivalence is recorded as an iff, and the identity-forces-two package is fed into two-prime branch controls, which in turn produce coherent prime orientation from prime-pair product cost consistency. Coherent orientation is part of the native-cost uniqueness blocker certificate and appears in the conditional universal-foundation certificate.
In the broader RS forcing picture, locking the orbit-$2$ axis is the discrete step that prevents mixed identity/reciprocal prime orientations from spoiling uniqueness of the native cost (the $J$-cost fixed by T5 and the Recognition Composition Law). The declaration does not itself prove uniqueness; it only lowers the hypothesis burden from a global exclusion Prop to a witness-level exclusion Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.